src/FOLP/ex/Intro.thy
changeset 58957 c9e744ea8a38
parent 58889 5b7a9633cfa8
child 60770 240563fbf41d
     1.1 --- a/src/FOLP/ex/Intro.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOLP/ex/Intro.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -45,13 +45,13 @@
     1.4  
     1.5  schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
     1.6          -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
     1.7 -apply (tactic {* fast_tac FOLP_cs 1 *})
     1.8 +apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
     1.9  done
    1.10  
    1.11  
    1.12  schematic_lemma "?p : ALL x. P(x,f(x)) <->
    1.13          (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
    1.14 -apply (tactic {* fast_tac FOLP_cs 1 *})
    1.15 +apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
    1.16  done
    1.17  
    1.18