| author | wenzelm |
| Wed, 27 Jun 2012 17:36:46 +0200 | |
| changeset 48160 | ac561771abdb |
| parent 47232 | e2f0176149d0 |
| permissions | -rw-r--r-- |
| 37694 | 1 |
|
2 |
(* Classical Higher-order Logic -- batteries included *) |
|
3 |
||
| 47232 | 4 |
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", |
| 44006 | 5 |
"Product_Lattice", |
| 45985 | 6 |
"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*), |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45985
diff
changeset
|
7 |
"Code_Real_Approx_By_Float", "Target_Numeral"]; |