1 (* Title: CalcElements/theoryC.sml |
1 (* Title: CalcElements/theoryC.sml |
2 Author: Walther Neuper |
2 Author: Walther Neuper |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 |
4 |
5 TODO: use "ThyC" for renaming identifiers. |
5 Probably this structure can be dropped due to improved reflection in Isabelle. |
6 Probably this structure can be dropped due to improvements of Isabelle. |
|
7 *) |
6 *) |
8 signature THEORY_ISAC = |
7 signature THEORY_ISAC = |
9 sig |
8 sig |
10 eqtype thyID |
9 eqtype thyID |
11 eqtype domID |
10 eqtype domID |
37 (**) |
36 (**) |
38 |
37 |
39 (* Since Isabelle2017 sessions in theory identifiers are enforced. |
38 (* Since Isabelle2017 sessions in theory identifiers are enforced. |
40 However, we leave theory identifiers short, in particular in use as keys into KEStore. *) |
39 However, we leave theory identifiers short, in particular in use as keys into KEStore. *) |
41 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID) |
40 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID) |
|
41 |
42 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*) |
42 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*) |
43 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*) |
43 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*) |
44 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*) |
44 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*) |
45 (*ad thm': |
|
46 there are two kinds of theorems ... |
|
47 (1) known by isabelle |
|
48 (2) not known, eg. calc_thm, instantiated rls |
|
49 the latter have a thmid "#..." |
|
50 and thus outside isa we ALWAYS transport both (thmID, ThmC.string_of_thmI) |
|
51 and have a special assoc_thm / assoc_rls in this interface *) |
|
52 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*) |
45 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*) |
53 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) |
46 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) |
54 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) |
47 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) |
55 val e_domID = "e_domID" : domID; |
48 val e_domID = "e_domID" : domID; |
56 fun string_of_thy thy = Context.theory_name thy: theory'; |
49 fun string_of_thy thy = Context.theory_name thy: theory'; |