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 60151 9023d59acce6
parent 60147 6d7b7a037e8d
child 60169 5ef8ed685965 
--- a/src/HOL/Extraction.thy	Tue Apr 28 16:23:38 2015 +0100
+++ b/src/HOL/Extraction.thy	Tue Apr 28 19:09:28 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 implies_False_swap
+  False_implies_equals
 
 lemmas [extraction_expand_def] =
   HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
isabelle