equal
deleted
inserted
replaced
272 datatype istate = (*interpreter state*) |
272 datatype istate = (*interpreter state*) |
273 Uistate (*undefined in modspec, in '_deriv'ation*) |
273 Uistate (*undefined in modspec, in '_deriv'ation*) |
274 | ScrState of scrstate (*for script interpreter*) |
274 | ScrState of scrstate (*for script interpreter*) |
275 | RrlsState of rrlsstate; (*for reverse rewriting*) |
275 | RrlsState of rrlsstate; (*for reverse rewriting*) |
276 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate; |
276 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate; |
277 val e_ctxt = ProofContext.init_global @{theory}; |
277 val e_ctxt = ProofContext.init_global @{theory "Pure"}; |
|
278 |
|
279 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*) |
|
280 fun is_e_ctxt ctxt = Theory.eq_thy (ProofContext.theory_of ctxt, @{theory "Pure"}); |
278 |
281 |
279 type iist = istate option * istate option; |
282 type iist = istate option * istate option; |
280 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) |
283 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) |
281 |
284 |
282 |
285 |