79 fun parent_path flat_names = if flat_names then I else Theory.parent_path; |
79 fun parent_path flat_names = if flat_names then I else Theory.parent_path; |
80 |
80 |
81 |
81 |
82 (* store theorems in theory *) |
82 (* store theorems in theory *) |
83 |
83 |
84 fun store_thmss_atts label tnames attss thmss thy = |
84 fun store_thmss_atts label tnames attss thmss = |
85 (thy, tnames ~~ attss ~~ thmss) |> |
85 fold_map (fn ((tname, atts), thms) => |
86 foldl_map (fn (thy', ((tname, atts), thms)) => thy' |> |
86 Theory.add_path tname |
87 Theory.add_path tname |> |
87 #> PureThy.add_thmss [((label, thms), atts)] |
88 (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>> |
88 #-> (fn thm::_ => Theory.parent_path #> pair thm) |
89 Theory.parent_path) |> Library.swap; |
89 ) (tnames ~~ attss ~~ thmss); |
90 |
90 |
91 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []); |
91 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []); |
92 |
92 |
93 fun store_thms_atts label tnames attss thms thy = |
93 fun store_thms_atts label tnames attss thmss = |
94 (thy, tnames ~~ attss ~~ thms) |> |
94 fold_map (fn ((tname, atts), thms) => |
95 foldl_map (fn (thy', ((tname, atts), thm)) => thy' |> |
95 Theory.add_path tname |
96 Theory.add_path tname |> |
96 #> PureThy.add_thms [((label, thms), atts)] |
97 (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>> |
97 #-> (fn thm::_ => Theory.parent_path #> pair thm) |
98 Theory.parent_path) |> Library.swap; |
98 ) (tnames ~~ attss ~~ thmss); |
99 |
99 |
100 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []); |
100 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []); |
101 |
101 |
102 |
102 |
103 (* split theorem thm_1 & ... & thm_n into n theorems *) |
103 (* split theorem thm_1 & ... & thm_n into n theorems *) |