src/HOL/Library/normarith.ML
changeset 31293 198eae6f5a35
parent 31118 541d43bee678
child 31344 fc09ec06b89b
equal deleted inserted replaced
31292:d24b2692562f 31293:198eae6f5a35
   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_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 dist_vector_def}, @{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 =