src/FOLP/ex/If.thy
changeset 58957 c9e744ea8a38
parent 36319 8feb2c4bef1a
child 60770 240563fbf41d
     1.1 --- a/src/FOLP/ex/If.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOLP/ex/If.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
     1.5    shows "?p : if(P,Q,R)"
     1.6  apply (unfold if_def)
     1.7 -apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
     1.8 +apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
     1.9  done
    1.10  
    1.11  schematic_lemma ifE:
    1.12 @@ -19,7 +19,7 @@
    1.13    shows "?p : S"
    1.14  apply (insert 1)
    1.15  apply (unfold if_def)
    1.16 -apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
    1.17 +apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
    1.18  done
    1.19  
    1.20  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))"
    1.21 @@ -33,11 +33,11 @@
    1.22  ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
    1.23  
    1.24  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))"
    1.25 -apply (tactic {* fast_tac if_cs 1 *})
    1.26 +apply (tactic {* fast_tac @{context} if_cs 1 *})
    1.27  done
    1.28  
    1.29  schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    1.30 -apply (tactic {* fast_tac if_cs 1 *})
    1.31 +apply (tactic {* fast_tac @{context} if_cs 1 *})
    1.32  done
    1.33  
    1.34  end