[isabelle] Isar and theories




I'm currently engaged in converting some of my Isabelle proof scripts into Isar.

So, for example, I get

  apply (tactic
    "(TRYALL (dres_inst_tac [(\"x\", \"0\")] fun_cong THEN'
      Force_tac))") ;
  apply (tactic "(TRYALL (etac notE))") ;
  apply (tactic "(TRYALL (EVERY' [ rtac ext,
    dres_inst_tac [(\"x\", \"Suc ?x\")] fun_cong,
    Force_tac]))") ;

Now this works, when entered during an interactive session.
It doesn't work, when it is part of a theory file.

Now this is something to do with the current theory context.
Because when I change it to

  apply (tactic
    "(TRYALL (dres_inst_tac [(\"x\", \"0\")] fun_cong THEN'
      CLASIMPSET' force_tac))") ;
  apply (tactic "(TRYALL (etac notE))") ;
  apply (tactic "(TRYALL (EVERY' [ rtac ext,
    dres_inst_tac [(\"x\", \"Suc ?x\")] fun_cong,
    CLASIMPSET' force_tac]))") ;

it does work.

However I would very much like to know why.

Any help would be appreciated.

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.