| changeset 37763 | 38456e144423 |
| parent 37694 | 19e8b730ddeb |
| child 38119 | e00f970425e9 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/HOL_Library_ROOT.ML Sat Jul 10 22:39:16 2010 +0200 @@ -0,0 +1,5 @@ + +(* Classical Higher-order Logic -- batteries included *) + +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", + "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];