src/FOL/FOL.thy
changeset 18531 ce7b80b7c84e
parent 18522 9bdfb6eaf8ab
child 18591 04b9f2bf5a48
equal deleted inserted replaced
18530:d995aecddc15 18531:ce7b80b7c84e
    21 
    21 
    22 subsection {* Lemmas and proof tools *}
    22 subsection {* Lemmas and proof tools *}
    23 
    23 
    24 use "FOL_lemmas1.ML"
    24 use "FOL_lemmas1.ML"
    25 theorems case_split = case_split_thm [case_names True False, cases type: o]
    25 theorems case_split = case_split_thm [case_names True False, cases type: o]
    26 
       
    27 lemma cla_dist_concl:
       
    28   assumes x: "~Z_Z ==> PROP X_X"
       
    29     and z: "PROP Y_Y ==> Z_Z"
       
    30     and y: "PROP X_X ==> PROP Y_Y"
       
    31   shows Z_Z
       
    32   apply (rule classical)
       
    33   apply (erule x [THEN y, THEN z])
       
    34   done
       
    35 
    26 
    36 use "cladata.ML"
    27 use "cladata.ML"
    37 setup Cla.setup
    28 setup Cla.setup
    38 setup cla_setup
    29 setup cla_setup
    39 setup case_setup
    30 setup case_setup