equal
deleted
inserted
replaced
39 apply (drule spec) |
39 apply (drule spec) |
40 apply assumption |
40 apply assumption |
41 done |
41 done |
42 |
42 |
43 |
43 |
44 subsubsection \<open>Demonstration of @{text "fast"}\<close> |
44 subsubsection \<open>Demonstration of \<open>fast\<close>\<close> |
45 |
45 |
46 schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x)) |
46 schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x)) |
47 --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" |
47 --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" |
48 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
48 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
49 done |
49 done |