61 let |
61 let |
62 val fun_ids = Specify.get_fun_ids thy |
62 val fun_ids = Specify.get_fun_ids thy |
63 in |
63 in |
64 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy |
64 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy |
65 andalso not (thm contains_one_of fun_ids) |
65 andalso not (thm contains_one_of fun_ids) |
66 andalso not (ThmC.thmID_of_derivation_name' thm = "mono")) |
66 andalso not (ThmC.id_of_thm thm = "mono")) |
67 (* created in Biegelinie by partial_function ^^^^^^*) |
67 (* created in Biegelinie by partial_function ^^^^^^*) |
68 (map snd (Global_Theory.all_thms_of thy false)) |
68 (map snd (Global_Theory.all_thms_of thy false)) |
69 end |
69 end |
70 |
70 |
71 (* wrap theory-data into the uniform type thydata *) |
71 (* wrap theory-data into the uniform type thydata *) |
72 |
72 |
73 fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) = |
73 fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) = |
74 let val theID = [part, thyID, "Theorems"] @ [ThmC.thmID_of_derivation_name' thm] : Celem.theID |
74 let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Celem.theID |
75 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], |
75 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], |
76 mathauthors = ["isac-team"], fillpats = [], thm = thm}) |
76 mathauthors = ["isac-team"], fillpats = [], thm = thm}) |
77 end; |
77 end; |
78 fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) = |
78 fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) = |
79 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID |
79 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID |
93 |
93 |
94 (* get all theorems from the list of rule-sets (defined in Knowledge) *) |
94 (* get all theorems from the list of rule-sets (defined in Knowledge) *) |
95 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list) |
95 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list) |
96 |> map (Rtools.thms_of_rls o #2 o #2) |
96 |> map (Rtools.thms_of_rls o #2 o #2) |
97 |> flat |
97 |> flat |
98 |> map (ThmC.revert_sym thy) |
98 |> map (ThmC.revert_sym_rule thy) |
99 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)) |
99 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)) |
100 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) |
100 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) |
101 : ThmC.T list |
101 : ThmC.T list |
102 |
102 |
103 (* collect all thydata defined in in a theory *) |
103 (* collect all thydata defined in in a theory *) |
121 [(*TODO: collect_cals, collect_ords*)] |
121 [(*TODO: collect_cals, collect_ords*)] |
122 |
122 |
123 (* collect theorems defined in Isabelle *) |
123 (* collect theorems defined in Isabelle *) |
124 fun collect_isab isa (thmDeriv, thm) = |
124 fun collect_isab isa (thmDeriv, thm) = |
125 let val theID = |
125 let val theID = |
126 [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.thmID_of_derivation_name thmDeriv] |
126 [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.cut_id thmDeriv] |
127 in |
127 in |
128 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID, |
128 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID, |
129 mathauthors = ["Isabelle team, TU Munich"], |
129 mathauthors = ["Isabelle team, TU Munich"], |
130 coursedesign = [], |
130 coursedesign = [], |
131 fillpats = [], |
131 fillpats = [], |