| author | blanchet |
| Mon, 09 Aug 2010 09:57:38 +0200 | |
| changeset 38275 | 1954191fc6cf |
| parent 38137 | 6fda94059baa |
| 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"]; |