equal
deleted
inserted
replaced
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 (*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*) |
|
22 time_use_thy "ex/Bin"; |
20 time_use_thy "ex/Bin"; |
23 |
21 |
24 (** Datatypes **) |
22 (** Datatypes **) |
25 time_use_thy "ex/BT"; (*binary trees*) |
23 time_use_thy "ex/BT"; (*binary trees*) |
26 time_use_thy "ex/Data"; (*Sample datatype*) |
24 time_use_thy "ex/Data"; (*Sample datatype*) |