[isabelle] Strange Behaviour of ALLGOALS



Dear all,

I encountered a strange behaviour of ALLGOALS under
Isabelle/HOL 2008.

  apply(tactic "ALLGOALS(COND' contains_eval thyp_ify (K all_tac))")

results in the error message:

*** Unknown context
*** At command "apply".


while each individual call:

  apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 4")
  apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 3")
  apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 2")
  apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 1")

works fine.

According specification in tctical.ML, they should behave the same ...

Can you help me?


bu


PS: In case that you need slightly more context
(but it should actually not matter):

ML{*
fun COND' C T1 T2 n = COND (C n) (T1 n) (T2 n);
fun contains_eval n thm =
    let fun T("Natural.evalc",_) = true | T _ = false
    in  Term.exists_Const T (term_of(cprem_of thm n)) end*}







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