changeset 1582 | 97a305db0c9e |
parent 1528 | 608dd813b437 |
child 1595 | b9984b1dbc4c |
1581:a82618a900e5 | 1582:97a305db0c9e |
---|---|
35 use "logic.ML"; |
35 use "logic.ML"; |
36 use "theory.ML"; |
36 use "theory.ML"; |
37 use "thm.ML"; |
37 use "thm.ML"; |
38 use "drule.ML"; |
38 use "drule.ML"; |
39 use "tctical.ML"; |
39 use "tctical.ML"; |
40 use "search.ML"; |
|
40 use "tactic.ML"; |
41 use "tactic.ML"; |
41 use "goals.ML"; |
42 use "goals.ML"; |
42 use "axclass.ML"; |
43 use "axclass.ML"; |
43 |
44 |
44 structure Pure = struct val thy = Theory.pure_thy end; |
45 structure Pure = struct val thy = Theory.pure_thy end; |