remove codegeneration-related theories from big library theory
authorhaftmann
Fri, 02 Jul 2010 14:23:17 +0200
changeset 37693 b10444eb9c98
parent 37692 7b072f0c8bde
child 37694 19e8b730ddeb
remove codegeneration-related theories from big library theory
src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Jul 02 14:23:17 2010 +0200
+++ b/src/HOL/Library/Library.thy	Fri Jul 02 14:23:17 2010 +0200
@@ -8,18 +8,14 @@
   Bit
   Boolean_Algebra
   Char_ord
-  Code_Char_chr
-  Code_Integer
   Continuity
   ContNotDenum
   Convex
   Countable
   Diagonalize
   Dlist
-  Efficient_Nat
   Enum
   Eval_Witness
-  Executable_Set
   Float
   Formal_Power_Series
   Fraction_Field