| author | bulwahn |
| Tue, 07 Jun 2011 14:06:12 +0200 | |
| changeset 43244 | db041e88a805 |
| parent 42841 | 9079f49053e5 |
| child 44006 | b9839fad3bb6 |
| permissions | -rw-r--r-- |
| 37694 | 1 |
|
2 |
(* Classical Higher-order Logic -- batteries included *) |
|
3 |
||
4 |
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", |
|
|
42841
9079f49053e5
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn
parents:
38504
diff
changeset
|
5 |
"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)]; |