# HG changeset patch
# User bulwahn
# Date 1280650544 -7200
# Node ID e00f970425e92be03b60595ebaa25a59162fae91
# Parent  561aa8eb63d3777ef678bc2ede9ec319685b91b2
adding Code_Prolog theory to IsaMakefile and HOL-Library root file

diff -r 561aa8eb63d3 -r e00f970425e9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Aug 01 10:15:43 2010 +0200
+++ b/src/HOL/IsaMakefile	Sun Aug 01 10:15:44 2010 +0200
@@ -401,7 +401,8 @@
   Library/AssocList.thy	Library/BigO.thy Library/Binomial.thy		\
   Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
-  Library/Code_Integer.thy Library/Code_Natural.thy			\
+  Library/Code_Integer.thy Library/Code_Natural.thy 			\
+  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	\
diff -r 561aa8eb63d3 -r e00f970425e9 src/HOL/Library/HOL_Library_ROOT.ML
--- a/src/HOL/Library/HOL_Library_ROOT.ML	Sun Aug 01 10:15:43 2010 +0200
+++ b/src/HOL/Library/HOL_Library_ROOT.ML	Sun Aug 01 10:15:44 2010 +0200
@@ -2,4 +2,4 @@
 (* Classical Higher-order Logic -- batteries included *)
 
 use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
-  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];
+  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];