equal
deleted
inserted
replaced
517 rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms))) |
517 rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms))) |
518 (* once again try the same rule, e.g. associativity against "()"*) |
518 (* once again try the same rule, e.g. associativity against "()"*) |
519 | Rule.Eval (cc as (op_, _)) => |
519 | Rule.Eval (cc as (op_, _)) => |
520 let val _= trace1 i (" try calc: " ^ op_ ^ "'") |
520 let val _= trace1 i (" try calc: " ^ op_ ^ "'") |
521 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*) |
521 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*) |
522 in case Eval.adhoc_thm thy cc ct of |
522 in case Eval.adhoc_thm ctxt cc ct of |
523 NONE => rew_once ruls asm ct apno thms |
523 NONE => rew_once ruls asm ct apno thms |
524 | SOME (_, thm') => |
524 | SOME (_, thm') => |
525 let |
525 let |
526 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) |
526 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) |
527 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; |
527 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; |
531 in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end |
531 in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end |
532 end |
532 end |
533 | Rule.Cal1 (cc as (op_, _)) => |
533 | Rule.Cal1 (cc as (op_, _)) => |
534 let val _= trace1 i (" try cal1: " ^ op_ ^ "'"); |
534 let val _= trace1 i (" try cal1: " ^ op_ ^ "'"); |
535 val ct = TermC.uminus_to_string ct |
535 val ct = TermC.uminus_to_string ct |
536 in case Eval.adhoc_thm1_ thy cc ct of |
536 in case Eval.adhoc_thm1_ @{context} cc ct of |
537 NONE => (ct, asm) |
537 NONE => (ct, asm) |
538 | SOME (_, thm') => |
538 | SOME (_, thm') => |
539 let |
539 let |
540 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) |
540 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls) |
541 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; |
541 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct; |