equal
deleted
inserted
replaced
49 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
49 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
50 type penv |
50 type penv |
51 val penv2str_ : Proof.context -> penv -> string (* NONE *) |
51 val penv2str_ : Proof.context -> penv -> string (* NONE *) |
52 type preori |
52 type preori |
53 val preoris2str : preori list -> string |
53 val preoris2str : preori list -> string |
54 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*) |
54 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
55 (* NONE *) |
55 (* NONE *) |
56 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
56 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
57 |
57 |
58 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
58 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
59 val untouched : itm list -> bool |
59 val untouched : itm list -> bool |
60 type envv |
60 type envv |
61 val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv |
61 val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv |