src/HOL/HOL.thy
changeset 45607 16b4f5774621
parent 45294 3c5d3d286055
child 45625 750c5a47400b
     1.1 --- a/src/HOL/HOL.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -494,7 +494,7 @@
     1.4  apply assumption
     1.5  done
     1.6  
     1.7 -lemmas ccontr = FalseE [THEN classical, standard]
     1.8 +lemmas ccontr = FalseE [THEN classical]
     1.9  
    1.10  (*notE with premises exchanged; it discharges ~R so that it can be used to
    1.11    make elimination rules*)
    1.12 @@ -1445,8 +1445,8 @@
    1.13  
    1.14  lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
    1.15  lemmas induct_atomize = induct_atomize' induct_equal_eq
    1.16 -lemmas induct_rulify' [symmetric, standard] = induct_atomize'
    1.17 -lemmas induct_rulify [symmetric, standard] = induct_atomize
    1.18 +lemmas induct_rulify' [symmetric] = induct_atomize'
    1.19 +lemmas induct_rulify [symmetric] = induct_atomize
    1.20  lemmas induct_rulify_fallback =
    1.21    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.22    induct_true_def induct_false_def