author | bulwahn |
Wed, 14 Dec 2011 16:30:32 +0100 | |
changeset 45873 | 37ffb8797a63 |
parent 45483 | 34d07cf7d207 |
child 45985 | 2d399a776de2 |
permissions | -rw-r--r-- |
37694 | 1 |
|
2 |
(* Classical Higher-order Logic -- batteries included *) |
|
3 |
||
44561
73f84bf0c6ac
avoid loading List_Cset and Dlist_Cet at the same time
haftmann
parents:
44006
diff
changeset
|
4 |
use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order", |
44006 | 5 |
"Product_Lattice", |
45483 | 6 |
"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*), |
7 |
"Code_Real_Approx_By_Float" ]; |