remove codegeneration-related theories from big library theory
authorhaftmann
Fri, 02 Jul 2010 14:23:17 +0200
changeset 37684b10444eb9c98
parent 37683 7b072f0c8bde
child 37685 19e8b730ddeb
remove codegeneration-related theories from big library theory
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/Library/Library.thy	Fri Jul 02 14:23:17 2010 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Fri Jul 02 14:23:17 2010 +0200
     1.3 @@ -8,18 +8,14 @@
     1.4    Bit
     1.5    Boolean_Algebra
     1.6    Char_ord
     1.7 -  Code_Char_chr
     1.8 -  Code_Integer
     1.9    Continuity
    1.10    ContNotDenum
    1.11    Convex
    1.12    Countable
    1.13    Diagonalize
    1.14    Dlist
    1.15 -  Efficient_Nat
    1.16    Enum
    1.17    Eval_Witness
    1.18 -  Executable_Set
    1.19    Float
    1.20    Formal_Power_Series
    1.21    Fraction_Field