src/HOL/Extraction.thy
changeset 60151 9023d59acce6
parent 60147 6d7b7a037e8d
child 60169 5ef8ed685965
     1.1 --- a/src/HOL/Extraction.thy	Tue Apr 28 16:23:38 2015 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Tue Apr 28 19:09:28 2015 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    induct_atomize induct_atomize' induct_rulify induct_rulify'
     1.5    induct_rulify_fallback induct_trueI
     1.6    True_implies_equals implies_True_equals TrueE
     1.7 -  False_implies_equals implies_False_swap
     1.8 +  False_implies_equals
     1.9  
    1.10  lemmas [extraction_expand_def] =
    1.11    HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def