equal
deleted
inserted
replaced
34 apply assumption |
34 apply assumption |
35 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
35 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
36 done |
36 done |
37 |
37 |
38 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
38 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
39 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
39 by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>) |
40 |
40 |
41 text\<open>Example of Dyckhoff's method\<close> |
41 text\<open>Example of Dyckhoff's method\<close> |
42 lemma "~ ~ ((P-->Q) | (Q-->P))" |
42 lemma "~ ~ ((P-->Q) | (Q-->P))" |
43 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
43 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> |
44 apply (unfold not_def) |
44 apply (unfold not_def) |