equal
deleted
inserted
replaced
14 loadpath := [".", "ex"]; |
14 loadpath := [".", "ex"]; |
15 |
15 |
16 time_use "ex/misc.ML"; |
16 time_use "ex/misc.ML"; |
17 time_use_thy "ex/Ramsey"; |
17 time_use_thy "ex/Ramsey"; |
18 |
18 |
19 (*Equivalence classes; integers; Binary integer arithmetic*) |
19 (*Integers & Binary integer arithmetic*) |
|
20 use "ex/twos_compl.ML"; (*can delete after autoloader change |
|
21 and addition of "twos_compl" to Bin.thy*) |
20 time_use_thy "ex/Bin"; |
22 time_use_thy "ex/Bin"; |
21 |
23 |
22 (** Datatypes **) |
24 (** Datatypes **) |
23 time_use_thy "ex/BT"; (*binary trees*) |
25 time_use_thy "ex/BT"; (*binary trees*) |
24 time_use_thy "ex/Data"; (*Sample datatype*) |
26 time_use_thy "ex/Data"; (*Sample datatype*) |