1.1 --- a/src/HOL/Extraction.thy	Fri May 01 20:26:06 2015 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Sun May 03 15:38:25 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
     1.8 +  False_implies_equals implies_False_swap
     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