14 | Hord of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool} |
14 | Hord of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool} |
15 | Hrls of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T} |
15 | Hrls of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T} |
16 | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Celem2.guh, mathauthors: authors, thm: thm} |
16 | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Celem2.guh, mathauthors: authors, thm: thm} |
17 | Html of {coursedesign: authors, guh: Celem2.guh, html: string, mathauthors: authors} |
17 | Html of {coursedesign: authors, guh: Celem2.guh, html: string, mathauthors: authors} |
18 type theID |
18 type theID |
|
19 val theID2str: string list -> string |
19 val the2str: thydata -> string |
20 val the2str: thydata -> string |
20 val thes2str: thydata list -> string |
21 val thes2str: thydata list -> string |
21 val theID2thyID: theID -> ThyC.id |
22 val theID2thyID: theID -> ThyC.id |
|
23 |
|
24 val part2guh: theID -> Celem2.guh |
|
25 val thy2guh: theID -> Celem2.guh |
|
26 val thypart2guh: theID -> Celem2.guh |
|
27 val thm2guh: string * ThyC.id -> ThmC_Def.id -> Celem2.guh |
|
28 val rls2guh: string * ThyC.id -> Rule_Set.id -> Celem2.guh |
|
29 val cal2guh: string * ThyC.id -> string -> Celem2.guh |
|
30 val ord2guh: string * ThyC.id -> string -> Celem2.guh |
|
31 val theID2guh: theID -> Celem2.guh |
|
32 |
22 val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list |
33 val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list |
23 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata |
34 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata |
24 (*\------- to Celem8 -------/*) |
35 (*\------- to Celem8 -------/*) |
25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
36 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
26 (*NONE*) |
37 (*NONE*) |