equal
deleted
inserted
replaced
54 val theID2str: string list -> string |
54 val theID2str: string list -> string |
55 val the2str: thydata -> string |
55 val the2str: thydata -> string |
56 val trace_calc: bool Unsynchronized.ref |
56 val trace_calc: bool Unsynchronized.ref |
57 eqtype thmID |
57 eqtype thmID |
58 type thm' |
58 type thm' |
59 datatype lrd = D | L | R |
|
60 val trace_rewrite: bool Unsynchronized.ref |
59 val trace_rewrite: bool Unsynchronized.ref |
61 val depth: int Unsynchronized.ref |
60 val depth: int Unsynchronized.ref |
62 val assoc_thy: Rule.theory' -> theory |
61 val assoc_thy: Rule.theory' -> theory |
63 type path |
|
64 val path2str: path -> string |
|
65 type thm'' |
62 type thm'' |
66 val metID2str: string list -> string |
63 val metID2str: string list -> string |
67 val e_pblID: pblID |
64 val e_pblID: pblID |
68 val e_metID: metID |
65 val e_metID: metID |
69 val empty_spec: spec |
66 val empty_spec: spec |
454 (* switch for checking guhs unique before storing a pbl or met; |
451 (* switch for checking guhs unique before storing a pbl or met; |
455 set true at startup (done at begin of ROOT.ML) |
452 set true at startup (done at begin of ROOT.ML) |
456 set false for editing IsacKnowledge (done at end of ROOT.ML) *) |
453 set false for editing IsacKnowledge (done at end of ROOT.ML) *) |
457 val check_guhs_unique = Unsynchronized.ref true; |
454 val check_guhs_unique = Unsynchronized.ref true; |
458 |
455 |
459 |
|
460 datatype lrd = L (*t1 in "t1$t2"*) |
|
461 | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*) |
|
462 type path = lrd list; |
|
463 fun ldr2str L = "L" |
|
464 | ldr2str R = "R" |
|
465 | ldr2str D = "D"; |
|
466 fun path2str k = (strs2str' o (map ldr2str)) k; |
|
467 |
|
468 |
|
469 (* the pattern for an item of a problems model or a methods guard *) |
456 (* the pattern for an item of a problems model or a methods guard *) |
470 type pat = |
457 type pat = |
471 (string * (* field *) |
458 (string * (* field *) |
472 (term * (* description *) |
459 (term * (* description *) |
473 term)) (* id | arbitrary term *); |
460 term)) (* id | arbitrary term *); |