equal
deleted
inserted
replaced
95 (string -> term -> theory -> (string * term) option) |
95 (string -> term -> theory -> (string * term) option) |
96 | Rls_ of rls (*.ie. rule sets may be nested.*) |
96 | Rls_ of rls (*.ie. rule sets may be nested.*) |
97 and scr = |
97 and scr = |
98 EmptyScr |
98 EmptyScr |
99 | Prog of term (* for met *) |
99 | Prog of term (* for met *) |
100 | Rfuns of (* for Rrls*) |
100 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) |
101 {init_state : (* initialise for reverse rewriting by the Interpreter *) |
101 {init_state : (* initialise for reverse rewriting by the Interpreter *) |
102 term -> (* for this the rrlsstate is initialised: *) |
102 term -> (* for this the rrlsstate is initialised: *) |
103 term * (* the current formula: goes locate_gen -> next_tac via istate *) |
103 term * (* the current formula: goes locate_gen -> next_tac via istate *) |
104 term * (* the final formula *) |
104 term * (* the final formula *) |
105 rule list (* of reverse rewrite set (#1#) *) |
105 rule list (* of reverse rewrite set (#1#) *) |
192 |
192 |
193 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*) |
193 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*) |
194 |
194 |
195 val e_rule = Thm ("refl", @{thm refl}); |
195 val e_rule = Thm ("refl", @{thm refl}); |
196 fun id_of_thm (Thm (id, _)) = id |
196 fun id_of_thm (Thm (id, _)) = id |
197 | id_of_thm _ = error "id_of_thm"; |
197 | id_of_thm _ = error "error id_of_thm"; |
198 fun thm_of_thm (Thm (_, thm)) = thm |
198 fun thm_of_thm (Thm (_, thm)) = thm |
199 | thm_of_thm _ = error "thm_of_thm"; |
199 | thm_of_thm _ = error "error thm_of_thm"; |
200 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
200 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
201 |
201 |
202 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
202 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
203 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
203 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
204 |
204 |