author | wenzelm |
Tue, 03 Aug 2010 16:57:45 +0200 | |
changeset 38137 | 6fda94059baa |
parent 38119 | src/HOL/Library/HOL_Library_ROOT.ML@e00f970425e9 |
child 38504 | 76965c356d2a |
permissions | -rw-r--r-- |
37694 | 1 |
|
2 |
(* Classical Higher-order Logic -- batteries included *) |
|
3 |
||
4 |
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", |
|
38119
e00f970425e9
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
bulwahn
parents:
37763
diff
changeset
|
5 |
"Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"]; |