334 | ketype2str' Thy_ = "Theory" |
334 | ketype2str' Thy_ = "Theory" |
335 | ketype2str' Pbl_ = "Problem" |
335 | ketype2str' Pbl_ = "Problem" |
336 | ketype2str' Met_ = "Method"; |
336 | ketype2str' Met_ = "Method"; |
337 |
337 |
338 (*see 'How to manage theorys in subproblems' at 'type thyID'*) |
338 (*see 'How to manage theorys in subproblems' at 'type thyID'*) |
339 val theory' = ref ([]:(theory' * theory) list); |
339 val theory' = Unsynchronized.ref ([]:(theory' * theory) list); |
340 |
340 |
341 (*.all theories defined for Scripts, recorded in Scripts/Script.ML; |
341 (*.all theories defined for Scripts, recorded in Scripts/Script.ML; |
342 in order to distinguish them from general IsacKnowledge defined later on.*) |
342 in order to distinguish them from general IsacKnowledge defined later on.*) |
343 val script_thys = ref ([] : (theory' * theory) list); |
343 val script_thys = Unsynchronized.ref ([] : (theory' * theory) list); |
344 |
344 |
345 |
345 |
346 (*rewrite orders, also stored in 'type met' and type 'and rls' |
346 (*rewrite orders, also stored in 'type met' and type 'and rls' |
347 The association list is required for 'rewrite.."rew_ord"..' |
347 The association list is required for 'rewrite.."rew_ord"..' |
348 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
348 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
357 |
357 |
358 |
358 |
359 (*WN060120 a hack to get alltogether run again with minimal effort: |
359 (*WN060120 a hack to get alltogether run again with minimal effort: |
360 theory' is inserted for creating thy_hierarchy; calls for assoc_rls |
360 theory' is inserted for creating thy_hierarchy; calls for assoc_rls |
361 need not be called*) |
361 need not be called*) |
362 val ruleset' = ref ([]:(rls' * (theory' * rls)) list); |
362 val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list); |
363 |
363 |
364 (*FIXME.040207 calclist': used by prep_rls, NOT in met*) |
364 (*FIXME.040207 calclist': used by prep_rls, NOT in met*) |
365 val calclist'= ref ([]: calc list); |
365 val calclist'= Unsynchronized.ref ([]: calc list); |
366 |
366 |
367 (*.the hierarchy of thydata.*) |
367 (*.the hierarchy of thydata.*) |
368 |
368 |
369 (*.'a is for pbt | met.*) |
369 (*.'a is for pbt | met.*) |
370 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) |
370 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*) |
401 mathauthors: authors, |
401 mathauthors: authors, |
402 ord: (subst -> (term * term) -> bool)}; |
402 ord: (subst -> (term * term) -> bool)}; |
403 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; |
403 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; |
404 |
404 |
405 type thehier = (thydata ptyp) list; |
405 type thehier = (thydata ptyp) list; |
406 val thehier = ref ([] : thehier); |
406 val thehier = Unsynchronized.ref ([] : thehier); |
407 |
407 |
408 (*.an association list, gets the value once in Isac.ML.*) |
408 (*.an association list, gets the value once in Isac.ML.*) |
409 val isab_thm_thy = ref ([] : (thmID * (thyID * term)) list); |
409 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); |
410 |
410 |
411 |
411 |
412 type path = string; |
412 type path = string; |
413 type filename = string; |
413 type filename = string; |
414 |
414 |
630 |
630 |
631 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; |
631 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; |
632 |
632 |
633 |
633 |
634 (*.trace internal steps of isac's rewriter*) |
634 (*.trace internal steps of isac's rewriter*) |
635 val trace_rewrite = ref false; |
635 val trace_rewrite = Unsynchronized.ref false; |
636 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
636 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
637 val depth = ref 99999; |
637 val depth = Unsynchronized.ref 99999; |
638 (*.no of rewrites exceeding this int -> NO rewrite.*) |
638 (*.no of rewrites exceeding this int -> NO rewrite.*) |
639 (*WN060829 still unused...*) |
639 (*WN060829 still unused...*) |
640 val lim_rewrite = ref 99999; |
640 val lim_rewrite = Unsynchronized.ref 99999; |
641 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) |
641 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) |
642 val lim_deriv = ref 100; |
642 val lim_deriv = Unsynchronized.ref 100; |
643 (*.switch for checking guhs unique before storing a pbl or met; |
643 (*.switch for checking guhs unique before storing a pbl or met; |
644 set true at startup (done at begin of ROOT.ML) |
644 set true at startup (done at begin of ROOT.ML) |
645 set false for editing IsacKnowledge (done at end of ROOT.ML).*) |
645 set false for editing IsacKnowledge (done at end of ROOT.ML).*) |
646 val check_guhs_unique = ref false; |
646 val check_guhs_unique = Unsynchronized.ref false; |
647 |
647 |
648 |
648 |
649 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) |
649 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) |
650 L (*go left at $*) |
650 L (*go left at $*) |
651 | R (*go right at $*) |
651 | R (*go right at $*) |