115 scr : scr} (*Script term (how to restrict type ???)*) |
115 scr : scr} (*Script term (how to restrict type ???)*) |
116 (*Rrls call SML-code and simulate an rls |
116 (*Rrls call SML-code and simulate an rls |
117 difference: there is always _ONE_ redex rewritten in 1 call, |
117 difference: there is always _ONE_ redex rewritten in 1 call, |
118 thus wrap Rrls by: Rls (Rls_ ...)*) |
118 thus wrap Rrls by: Rls (Rls_ ...)*) |
119 |
119 |
120 | Rrls of (*for 'reverse rewriting' by SML-functions instead Script*) |
120 | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *) |
121 {id : string, (*for trace_rewrite:=true *) |
121 {id : string, (* for trace_rewrite := true *) |
122 prepat : (term list *(*preconds, eval with subst from pattern *) |
122 prepat : (term list *(* preconds, eval with subst from pattern; |
123 term ) (*pattern matched in subterms *) |
123 if [HOLogic.true_const], match decides alone *) |
124 list, (*meta-conjunction is or *) |
124 term ) (* pattern matched with current (sub)term *) |
125 rew_ord : rew_ord, (*for rules *) |
125 list, (* meta-conjunction is or *) |
126 erls : rls, (*for the conditions in rules and pat *) |
126 rew_ord : rew_ord, (* for rules *) |
127 (* '^ because of rewrite in applicable_in |
127 erls : rls, (* for the conditions in rules and preconds *) |
128 compare type met*) |
128 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *) |
129 calc : calc list, (*for Calculate in scr, set by prep_rls *) |
129 scr : scr}; (* Rfuns {...} (how to restrict type ???) *) |
130 scr : scr}; (*Rfuns {...} (how to restrict type ???)*) |
|
131 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently |
130 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently |
132 from rls, and then contain both Script _AND_ Rfuns !!!*) |
131 from rls, and then contain both Script _AND_ Rfuns !!!*) |
133 |
132 |
134 fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) |
133 fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) |
135 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) |
134 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) |