# HG changeset patch
# User haftmann
# Date 1259772814 -3600
# Node ID 7ed48b28bb7f3de503651c777ebe93cb7ff9af5e
# Parent  6e77ca6d3a8f8293d6799f1d319166481c36cb8e
added Crude_Executable_Set.thy

diff -r 6e77ca6d3a8f -r 7ed48b28bb7f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Nov 29 12:56:30 2009 +1100
+++ b/src/HOL/IsaMakefile	Wed Dec 02 17:53:34 2009 +0100
@@ -369,6 +369,7 @@
   Library/Sum_Of_Squares/sos_wrapper.ML					\
   Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
   Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy	\
+  Library/Crude_Executable_Set.thy					\
   Library/Infinite_Set.thy Library/FuncSet.thy				\
   Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
   Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
@@ -381,9 +382,9 @@
   Library/Order_Relation.thy Library/Nested_Environment.thy		\
   Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
   Library/Library/document/root.tex Library/Library/document/root.bib	\
-  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
-  Library/Product_ord.thy	Library/Char_nat.thy \
-  Library/Char_ord.thy Library/Option_ord.thy	\
+  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
+  Library/Product_ord.thy Library/Char_nat.thy				\
+  Library/Char_ord.thy Library/Option_ord.thy				\
   Library/Sublist_Order.thy Library/List_lexord.thy			\
   Library/Coinductive_List.thy Library/AssocList.thy			\
   Library/Formal_Power_Series.thy Library/Binomial.thy			\
diff -r 6e77ca6d3a8f -r 7ed48b28bb7f src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sun Nov 29 12:56:30 2009 +1100
+++ b/src/HOL/Library/Library.thy	Wed Dec 02 17:53:34 2009 +0100
@@ -14,6 +14,7 @@
   Continuity
   ContNotDenum
   Countable
+  Crude_Executable_Set
   Diagonalize
   Efficient_Nat
   Enum