# HG changeset patch
# User haftmann
# Date 1278073397 -7200
# Node ID b10444eb9c98be3c67ce2cf41b22f5d94c1f6414
# Parent  7b072f0c8bde21bae07de52e44dc9d10ce00846e
remove codegeneration-related theories from big library theory

diff -r 7b072f0c8bde -r b10444eb9c98 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