equal
deleted
inserted
replaced
577 fun fun_upd_prover ss = |
577 fun fun_upd_prover ss = |
578 rtac eq_reflection 1 THEN rtac ext 1 THEN |
578 rtac eq_reflection 1 THEN rtac ext 1 THEN |
579 simp_tac (Simplifier.inherit_context ss current_ss) 1 |
579 simp_tac (Simplifier.inherit_context ss current_ss) 1 |
580 in |
580 in |
581 val fun_upd2_simproc = |
581 val fun_upd2_simproc = |
582 Simplifier.simproc (Theory.sign_of (the_context ())) |
582 Simplifier.simproc @{theory} |
583 "fun_upd2" ["f(v := w, x := y)"] |
583 "fun_upd2" ["f(v := w, x := y)"] |
584 (fn _ => fn ss => fn t => |
584 (fn _ => fn ss => fn t => |
585 case find_double t of (T, NONE) => NONE |
585 case find_double t of (T, NONE) => NONE |
586 | (T, SOME rhs) => |
586 | (T, SOME rhs) => |
587 SOME (Goal.prove (Simplifier.the_context ss) [] [] |
587 SOME (Goal.prove (Simplifier.the_context ss) [] [] |