equal
deleted
inserted
replaced
242 | eq_Thm (Rls_ r1, _) = false |
242 | eq_Thm (Rls_ r1, _) = false |
243 | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^ |
243 | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^ |
244 (rule2str r1)^"' '"^(rule2str r2)^"'"); |
244 (rule2str r1)^"' '"^(rule2str r2)^"'"); |
245 fun distinct_Thm r = gen_distinct eq_Thm r; |
245 fun distinct_Thm r = gen_distinct eq_Thm r; |
246 |
246 |
247 fun eq_Thms thmIDs thm = (member op = (id_of_thm thm) thmIDs) |
247 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm)) |
248 handle _ => false; |
248 handle _ => false; |
249 |
249 |
250 |
250 |
251 (***. context to thy concerning rewriting .***) |
251 (***. context to thy concerning rewriting .***) |
252 |
252 |
719 |
719 |
720 fun guh2theID (guh:guh) = |
720 fun guh2theID (guh:guh) = |
721 let val guh' = explode guh |
721 let val guh' = explode guh |
722 val part = implode (take_fromto 1 4 guh') |
722 val part = implode (take_fromto 1 4 guh') |
723 val isa = implode (take_fromto 5 9 guh') |
723 val isa = implode (take_fromto 5 9 guh') |
724 in if not (member op = part ["exp_", "thy_", "pbl_", "met_"]) |
724 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part) |
725 then raise error ("guh '"^guh^"' does not begin with \ |
725 then raise error ("guh '"^guh^"' does not begin with \ |
726 \exp_ | thy_ | pbl_ | met_") |
726 \exp_ | thy_ | pbl_ | met_") |
727 else let val chap = case isa of |
727 else let val chap = case isa of |
728 "isab_" => "Isabelle" |
728 "isab_" => "Isabelle" |
729 | "scri_" => "IsacScripts" |
729 | "scri_" => "IsacScripts" |