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.
Expand proofs of induct_atomize'/rulify'.
authorberghofe
Sun, 10 Jan 2010 18:39:50 +0100
changeset 34913 d8cb720c9c53
parent 34912 c04747153bcf
child 34914 e391c3de0f6b
Expand proofs of induct_atomize'/rulify'.
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Sun Jan 10 18:37:37 2010 +0100
+++ b/src/HOL/Extraction.thy	Sun Jan 10 18:39:50 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Extraction.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 *)
 
@@ -28,11 +27,13 @@
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
   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_atomize induct_rulify induct_rulify_fallback
+  induct_atomize induct_atomize' induct_rulify induct_rulify'
+  induct_rulify_fallback induct_trueI
   True_implies_equals TrueE
 
 lemmas [extraction_expand_def] =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+  induct_true_def induct_false_def
 
 datatype sumbool = Left | Right
isabelle