Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
authorbulwahn
Sun, 01 Aug 2010 10:15:44 +0200
changeset 38119 e00f970425e9
parent 38118 561aa8eb63d3
child 38120 99440c205e4a
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Library/HOL_Library_ROOT.ML file | annotate | diff | comparison | revisions 
--- 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	\
--- 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"];
isabelle