# HG changeset patch
# User berghofe
# Date 1194948029 -3600
# Node ID 170f4cc346976d093f80fe29c6d45fff9eb7c3f5
# Parent  2c6167e2c5876217deae359d6f59e7f37e026428
Added TrueE to extraction_expand.

diff -r 2c6167e2c587 -r 170f4cc34697 src/HOL/Extraction.thy
--- 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