equal
deleted
inserted
replaced
16 |
16 |
17 (*Equivalence classes and integers*) |
17 (*Equivalence classes and integers*) |
18 time_use_thy "ex/equiv"; |
18 time_use_thy "ex/equiv"; |
19 time_use_thy "ex/integ"; |
19 time_use_thy "ex/integ"; |
20 (*Binary integer arithmetic*) |
20 (*Binary integer arithmetic*) |
21 use "ex/twos-compl.ML"; |
21 use "ex/twos_compl.ML"; |
22 time_use "ex/bin.ML"; |
22 time_use "ex/bin.ML"; |
23 time_use_thy "ex/binfn"; |
23 time_use_thy "ex/binfn"; |
24 |
24 |
25 (** Datatypes **) |
25 (** Datatypes **) |
26 (*binary trees*) |
26 (*binary trees*) |