equal
deleted
inserted
replaced
495 Simplifier.simproc (Theory.sign_of (the_context ())) |
495 Simplifier.simproc (Theory.sign_of (the_context ())) |
496 "fun_upd2" ["f(v := w, x := y)"] |
496 "fun_upd2" ["f(v := w, x := y)"] |
497 (fn sg => fn ss => fn t => |
497 (fn sg => fn ss => fn t => |
498 case find_double t of (T, NONE) => NONE |
498 case find_double t of (T, NONE) => NONE |
499 | (T, SOME rhs) => |
499 | (T, SOME rhs) => |
500 SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss)))) |
500 SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss)))) |
501 end; |
501 end; |
502 Addsimprocs[fun_upd2_simproc]; |
502 Addsimprocs[fun_upd2_simproc]; |
503 |
503 |
504 val expand_fun_eq = thm "expand_fun_eq"; |
504 val expand_fun_eq = thm "expand_fun_eq"; |
505 val apply_inverse = thm "apply_inverse"; |
505 val apply_inverse = thm "apply_inverse"; |