# HG changeset patch
# User bulwahn
# Date 1290422096 -3600
# Node ID d40b347d5b0b8c2f8b904b0b1b260fa46349858b
# Parent  dc1b5aa908ff23282b42b4ec35d305728f8a4cef
adding Enum to HOL-Main image and removing it from HOL-Library

diff -r dc1b5aa908ff -r d40b347d5b0b src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -3,7 +3,7 @@
 header {* Finite types as explicit enumerations *}
 
 theory Enum
-imports Map Main
+imports Map String
 begin
 
 subsection {* Class @{text enum} *}
diff -r dc1b5aa908ff -r d40b347d5b0b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 22 11:34:56 2010 +0100
@@ -246,6 +246,7 @@
   Divides.thy \
   DSequence.thy \
   Equiv_Relations.thy \
+  Enum.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
   Int.thy \
@@ -416,7 +417,7 @@
   Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
   Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
-  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
+  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
diff -r dc1b5aa908ff -r d40b347d5b0b src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Library/Library.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -14,7 +14,6 @@
   Countable
   Diagonalize
   Dlist
-  Enum
   Eval_Witness
   Float
   Formal_Power_Series
diff -r dc1b5aa908ff -r d40b347d5b0b src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:55 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Nov 22 11:34:56 2010 +0100
@@ -3,7 +3,7 @@
 header {* A simple counterexample generator *}
 
 theory Quickcheck
-imports Random Code_Evaluation
+imports Random Code_Evaluation Enum
 uses ("Tools/quickcheck_generators.ML")
 begin