src/FOLP/ex/Intro.thy
changeset 41526 54b4686704af
parent 36319 8feb2c4bef1a
child 58889 5b7a9633cfa8
equal deleted inserted replaced
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"