equal
deleted
inserted
replaced
34 apply assumption |
34 apply assumption |
35 --{* @{subgoals[display,indent=0,margin=65]} *} |
35 --{* @{subgoals[display,indent=0,margin=65]} *} |
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 {*IntPr.fast_tac 1*}) |
39 by (tactic {*IntPr.fast_tac @{context} 1*}) |
40 |
40 |
41 text{*Example of Dyckhoff's method*} |
41 text{*Example of Dyckhoff's method*} |
42 lemma "~ ~ ((P-->Q) | (Q-->P))" |
42 lemma "~ ~ ((P-->Q) | (Q-->P))" |
43 --{* @{subgoals[display,indent=0,margin=65]} *} |
43 --{* @{subgoals[display,indent=0,margin=65]} *} |
44 apply (unfold not_def) |
44 apply (unfold not_def) |