96 |
96 |
97 val pprint_theory = Sign.pprint_sg o sign_of; |
97 val pprint_theory = Sign.pprint_sg o sign_of; |
98 |
98 |
99 val print_syntax = Syntax.print_syntax o syn_of; |
99 val print_syntax = Syntax.print_syntax o syn_of; |
100 |
100 |
101 fun print_axioms thy = |
101 fun print_thy thy = |
102 let |
102 let |
103 val {sign, new_axioms, ...} = rep_theory thy; |
103 val {sign, new_axioms, oracles, ...} = rep_theory thy; |
104 val axioms = Symtab.dest new_axioms; |
104 val axioms = Symtab.dest new_axioms; |
|
105 val oras = map fst (Symtab.dest oracles); |
105 |
106 |
106 fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, |
107 fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, |
107 Pretty.quote (Sign.pretty_term sign t)]; |
108 Pretty.quote (Sign.pretty_term sign t)]; |
108 in |
109 in |
109 Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms)) |
110 Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms)); |
110 end; |
111 Pretty.writeln (Pretty.strs ("oracles:" :: oras)) |
111 |
112 end; |
112 fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy); |
113 |
|
114 fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy); |
113 |
115 |
114 |
116 |
115 |
117 |
116 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) |
118 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) |
117 |
119 |