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 TrueE to extraction_expand.
authorberghofe
Tue, 13 Nov 2007 11:00:29 +0100
changeset 25424 170f4cc34697
parent 25423 2c6167e2c587
child 25425 9191942c4ead
Added TrueE to extraction_expand.
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Tue Nov 13 10:59:26 2007 +0100
+++ b/src/HOL/Extraction.thy	Tue Nov 13 11:00:29 2007 +0100
@@ -55,7 +55,7 @@
   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
+  True_implies_equals TrueE
 
 datatype sumbool = Left | Right
isabelle