Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added eq_True eq_False True_implies_equals to extraction_expand
authorhaftmann
Tue, 10 Oct 2006 10:34:41 +0200
changeset 20941 beedcae49096
parent 20940 2526ef41a189
child 20942 43e216a9d615
added eq_True eq_False True_implies_equals to extraction_expand
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Tue Oct 10 10:24:24 2006 +0200
+++ b/src/HOL/Extraction.thy	Tue Oct 10 10:34:41 2006 +0200
@@ -51,10 +51,11 @@
 lemmas [extraction_expand] =
   atomize_eq atomize_all atomize_imp atomize_conj
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
-  notE' impE' impE iffE imp_cong simp_thms
+  notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
   induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   induct_atomize induct_rulify induct_rulify_fallback
+  True_implies_equals
 
 datatype sumbool = Left | Right
isabelle