equal
deleted
inserted
replaced
371 val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, |
371 val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, |
372 simp_tac ss 1] |
372 simp_tac ss 1] |
373 fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r) |
373 fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r) |
374 in |
374 in |
375 val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2" |
375 val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2" |
376 [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)] |
376 [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"] |
377 (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> |
377 (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> |
378 Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover)))) |
378 Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover)))) |
379 end; |
379 end; |
380 Addsimprocs[fun_upd2_simproc]; |
380 Addsimprocs[fun_upd2_simproc]; |
381 |
381 |