--- a/src/HOL/Extraction.thy Tue Apr 14 15:56:55 2015 +0200
+++ b/src/HOL/Extraction.thy Tue Apr 14 16:47:55 2015 +0200
@@ -31,7 +31,8 @@
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
induct_atomize induct_atomize' induct_rulify induct_rulify'
induct_rulify_fallback induct_trueI
- True_implies_equals TrueE
+ True_implies_equals implies_True_equals TrueE
+ False_implies_equals
lemmas [extraction_expand_def] =
HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def