changeset 41526 | 54b4686704af |
parent 36319 | 8feb2c4bef1a |
child 58889 | 5b7a9633cfa8 |
41525:a42cbf5b44c8 | 41526:54b4686704af |
---|---|
74 schematic_lemma |
74 schematic_lemma |
75 assumes "!!x. x : P ==> f(x) : False" |
75 assumes "!!x. x : P ==> f(x) : False" |
76 shows "?p : ~ P" |
76 shows "?p : ~ P" |
77 apply (unfold not_def) |
77 apply (unfold not_def) |
78 apply (rule impI) |
78 apply (rule impI) |
79 apply (rule prems) |
79 apply (rule assms) |
80 apply assumption |
80 apply assumption |
81 done |
81 done |
82 |
82 |
83 schematic_lemma |
83 schematic_lemma |
84 assumes major: "p : ~P" |
84 assumes major: "p : ~P" |