Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/normarith.ML
changeset 36936 c52d1c130898
parent 36753 5cf4e9128f22 
--- a/src/HOL/Library/normarith.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Library/normarith.ML	Sat May 15 17:59:06 2010 +0200
@@ -182,7 +182,6 @@
 fun botc1 conv ct = 
   ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
 
- fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct;
  val apply_pth1 = rewr_conv @{thm pth_1};
  val apply_pth2 = rewr_conv @{thm pth_2};
  val apply_pth3 = rewr_conv @{thm pth_3};
@@ -333,9 +332,9 @@
   in fst (RealArith.real_linear_prover translator
         (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
-        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
-        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
+        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
                        arg_conv (arg_conv real_poly_conv))) gts))
   end
 in val real_vector_combo_prover = real_vector_combo_prover
isabelle