equal
deleted
inserted
replaced
427 | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl")) |
427 | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl")) |
428 | context_thy (_, p) tac = |
428 | context_thy (_, p) tac = |
429 error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p) |
429 error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p) |
430 |
430 |
431 (* get all theorems in a rule set (recursivley containing rule sets) *) |
431 (* get all theorems in a rule set (recursivley containing rule sets) *) |
432 fun thm_of_rule Erule = [] |
432 fun thm_of_rule Celem.Erule = [] |
433 | thm_of_rule (thm as Celem.Thm _) = [thm] |
433 | thm_of_rule (thm as Celem.Thm _) = [thm] |
434 | thm_of_rule (Celem.Calc _) = [] |
434 | thm_of_rule (Celem.Calc _) = [] |
435 | thm_of_rule (Celem.Cal1 _) = [] |
435 | thm_of_rule (Celem.Cal1 _) = [] |
436 | thm_of_rule (Celem.Rls_ rls) = thms_of_rls rls |
436 | thm_of_rule (Celem.Rls_ rls) = thms_of_rls rls |
437 and thms_of_rls Celem.Erls = [] |
437 and thms_of_rls Celem.Erls = [] |