equal
deleted
inserted
replaced
102 val sym_trm : term -> term (* unused code, kept as hints to design ideas *) |
102 val sym_trm : term -> term (* unused code, kept as hints to design ideas *) |
103 |
103 |
104 val string_of_detail: Proof.context -> term -> string |
104 val string_of_detail: Proof.context -> term -> string |
105 (*from isac_test for Minisubpbl*) |
105 (*from isac_test for Minisubpbl*) |
106 val atom_typ: Proof.context -> typ -> unit |
106 val atom_typ: Proof.context -> typ -> unit |
|
107 val atom_trace_detail: Proof.context -> term -> unit |
107 |
108 |
108 \<^isac_test>\<open> |
109 \<^isac_test>\<open> |
109 val mk_negative: typ -> term -> term |
110 val mk_negative: typ -> term -> term |
110 val mk_Var: term -> term |
111 val mk_Var: term -> term |
111 val scala_of_term: term -> string |
112 val scala_of_term: term -> string |
112 |
113 |
113 val atom_write: Proof.context -> term -> unit |
114 val atom_write: Proof.context -> term -> unit |
114 val atom_trace: Proof.context -> term -> unit |
115 val atom_trace: Proof.context -> term -> unit |
115 |
116 |
116 val atom_write_detail: Proof.context -> term -> unit |
117 val atom_write_detail: Proof.context -> term -> unit |
117 val atom_trace_detail: Proof.context -> term -> unit |
118 (*val atom_trace_detail: Proof.context -> term -> unit*) |
118 \<close> |
119 \<close> |
119 end |
120 end |
120 |
121 |
121 (**) |
122 (**) |
122 structure TermC(**): TERM_ISAC(**) = |
123 structure TermC(**): TERM_ISAC(**) = |
219 fun atom_write _ t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
220 fun atom_write _ t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
220 fun atom_trace _ t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
221 fun atom_trace _ t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***"); |
221 end; |
222 end; |
222 |
223 |
223 fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t; |
224 fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t; |
|
225 \<close> |
224 fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t; |
226 fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t; |
225 \<close> |
|
226 |
227 |
227 (* contains the term a VAR(("*",_),_) ? *) |
228 (* contains the term a VAR(("*",_),_) ? *) |
228 fun contains_Var (Abs(_,_,body)) = contains_Var body |
229 fun contains_Var (Abs(_,_,body)) = contains_Var body |
229 | contains_Var (f $ f') = contains_Var f orelse contains_Var f' |
230 | contains_Var (f $ f') = contains_Var f orelse contains_Var f' |
230 | contains_Var (Var _) = true |
231 | contains_Var (Var _) = true |