prepared for more meta-simp rules (by Stefan Berghofer)
authornipkow
Tue Apr 14 16:47:55 2015 +0200 (2015-04-14)
changeset 6007073c6e58a105c
parent 60069 d76f9047121c
child 60071 323feed18a92
prepared for more meta-simp rules (by Stefan Berghofer)
src/HOL/Extraction.thy
     1.1 --- a/src/HOL/Extraction.thy	Tue Apr 14 15:56:55 2015 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Tue Apr 14 16:47:55 2015 +0200
     1.3 @@ -31,7 +31,8 @@
     1.4    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     1.5    induct_atomize induct_atomize' induct_rulify induct_rulify'
     1.6    induct_rulify_fallback induct_trueI
     1.7 -  True_implies_equals TrueE
     1.8 +  True_implies_equals implies_True_equals TrueE
     1.9 +  False_implies_equals
    1.10  
    1.11  lemmas [extraction_expand_def] =
    1.12    HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def