equal
deleted
inserted
replaced
389 (fold_rev (splitequation ctxt) eqs ges,gts) |
389 (fold_rev (splitequation ctxt) eqs ges,gts) |
390 end; |
390 end; |
391 |
391 |
392 fun init_conv ctxt = |
392 fun init_conv ctxt = |
393 Simplifier.rewrite (Simplifier.context ctxt |
393 Simplifier.rewrite (Simplifier.context ctxt |
394 (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_vector_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) |
394 (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) |
395 then_conv field_comp_conv |
395 then_conv field_comp_conv |
396 then_conv nnf_conv |
396 then_conv nnf_conv |
397 |
397 |
398 fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); |
398 fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); |
399 fun norm_arith ctxt ct = |
399 fun norm_arith ctxt ct = |