Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Extraction.thy
changeset 60147 6d7b7a037e8d
parent 60070 73c6e58a105c
child 60151 9023d59acce6 
--- a/src/HOL/Extraction.thy	Wed Apr 22 20:07:00 2015 +0200
+++ b/src/HOL/Extraction.thy	Sat Apr 25 17:38:22 2015 +0200
@@ -32,7 +32,7 @@
   induct_atomize induct_atomize' induct_rulify induct_rulify'
   induct_rulify_fallback induct_trueI
   True_implies_equals implies_True_equals TrueE
-  False_implies_equals
+  False_implies_equals implies_False_swap
 
 lemmas [extraction_expand_def] =
   HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
isabelle