adding Enum to HOL-Main image and removing it from HOL-Library
authorbulwahn
Mon Nov 22 11:34:56 2010 +0100 (2010-11-22)
changeset 40650d40b347d5b0b
parent 40649 dc1b5aa908ff
child 40651 9752ba7348b5
adding Enum to HOL-Main image and removing it from HOL-Library
src/HOL/Enum.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Quickcheck.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Nov 22 11:34:55 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:56 2010 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Finite types as explicit enumerations *}
     1.5  
     1.6  theory Enum
     1.7 -imports Map Main
     1.8 +imports Map String
     1.9  begin
    1.10  
    1.11  subsection {* Class @{text enum} *}
     2.1 --- a/src/HOL/IsaMakefile	Mon Nov 22 11:34:55 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Nov 22 11:34:56 2010 +0100
     2.3 @@ -246,6 +246,7 @@
     2.4    Divides.thy \
     2.5    DSequence.thy \
     2.6    Equiv_Relations.thy \
     2.7 +  Enum.thy \
     2.8    Groebner_Basis.thy \
     2.9    Hilbert_Choice.thy \
    2.10    Int.thy \
    2.11 @@ -416,7 +417,7 @@
    2.12    Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
    2.13    Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
    2.14    Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
    2.15 -  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
    2.16 +  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
    2.17    Library/Executable_Set.thy Library/Float.thy				\
    2.18    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    2.19    Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
     3.1 --- a/src/HOL/Library/Library.thy	Mon Nov 22 11:34:55 2010 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Mon Nov 22 11:34:56 2010 +0100
     3.3 @@ -14,7 +14,6 @@
     3.4    Countable
     3.5    Diagonalize
     3.6    Dlist
     3.7 -  Enum
     3.8    Eval_Witness
     3.9    Float
    3.10    Formal_Power_Series
     4.1 --- a/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:55 2010 +0100
     4.2 +++ b/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:56 2010 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4  header {* A simple counterexample generator *}
     4.5  
     4.6  theory Quickcheck
     4.7 -imports Random Code_Evaluation
     4.8 +imports Random Code_Evaluation Enum
     4.9  uses ("Tools/quickcheck_generators.ML")
    4.10  begin
    4.11