equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 signature BASIC_THEORY = |
9 signature BASIC_THEORY = |
10 sig |
10 sig |
11 type theory |
11 type theory |
12 type local_theory |
|
13 exception THEORY of string * theory list |
12 exception THEORY of string * theory list |
14 val rep_theory: theory -> |
13 val rep_theory: theory -> |
15 {sign: Sign.sg, |
14 {sign: Sign.sg, |
16 axioms: term Symtab.table, |
15 axioms: term Symtab.table, |
17 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, |
16 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, |
108 axioms: term Symtab.table, |
107 axioms: term Symtab.table, |
109 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, |
108 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, |
110 parents: theory list, |
109 parents: theory list, |
111 ancestors: theory list}; |
110 ancestors: theory list}; |
112 |
111 |
113 (*forward definition for Isar proof contexts*) |
|
114 type local_theory = theory * Object.T Symtab.table; |
|
115 |
|
116 fun make_theory sign axms oras parents ancestors = |
112 fun make_theory sign axms oras parents ancestors = |
117 Theory {sign = sign, axioms = axms, oracles = oras, |
113 Theory {sign = sign, axioms = axms, oracles = oras, |
118 parents = parents, ancestors = ancestors}; |
114 parents = parents, ancestors = ancestors}; |
119 |
115 |
120 fun rep_theory (Theory args) = args; |
116 fun rep_theory (Theory args) = args; |