diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/If.thy --- a/src/FOLP/ex/If.thy Sun Nov 09 14:08:00 2014 +0100 +++ b/src/FOLP/ex/If.thy Sun Nov 09 17:04:14 2014 +0100 @@ -9,7 +9,7 @@ assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R" shows "?p : if(P,Q,R)" apply (unfold if_def) -apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *}) +apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *}) done schematic_lemma ifE: @@ -19,7 +19,7 @@ shows "?p : S" apply (insert 1) apply (unfold if_def) -apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *}) +apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *}) done schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" @@ -33,11 +33,11 @@ ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *} schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" -apply (tactic {* fast_tac if_cs 1 *}) +apply (tactic {* fast_tac @{context} if_cs 1 *}) done schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" -apply (tactic {* fast_tac if_cs 1 *}) +apply (tactic {* fast_tac @{context} if_cs 1 *}) done end