# HG changeset patch # User wenzelm # Date 1635191891 -7200 # Node ID c14787d73db690d62e5f50fe5697c7c90da4ba54 # Parent 0eb2f18b18068417932da679cdabaaf0b5ae6a6b tuned; diff -r 0eb2f18b1806 -r c14787d73db6 src/Doc/Codegen/Computations.thy --- a/src/Doc/Codegen/Computations.thy Mon Oct 25 21:46:38 2021 +0200 +++ b/src/Doc/Codegen/Computations.thy Mon Oct 25 21:58:11 2021 +0200 @@ -274,7 +274,7 @@ fun raw_dvd (b, ct) = \<^instantiate>\x = ct and y = \if b then \<^cterm>\True\ else \<^cterm>\False\\ - in cterm "x \ y" for x y :: bool\; + in cterm \x \ y\ for x y :: bool\; val (_, dvd_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\dvd\, raw_dvd))); diff -r 0eb2f18b1806 -r c14787d73db6 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 25 21:46:38 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 25 21:58:11 2021 +0200 @@ -323,7 +323,7 @@ fun cterm_of_varpow x k = if k = 1 then x - else \<^instantiate>\x and k = \Numeral.mk_cnumber \<^ctyp>\nat\ k\ in cterm "x ^ k" for x :: real\ + else \<^instantiate>\x and k = \Numeral.mk_cnumber \<^ctyp>\nat\ k\ in cterm \x ^ k\ for x :: real\ fun cterm_of_monomial m = if FuncUtil.Ctermfunc.is_empty m then \<^cterm>\1::real\ @@ -331,13 +331,13 @@ let val m' = FuncUtil.dest_monomial m val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] - in foldr1 (fn (s, t) => \<^instantiate>\s and t in cterm "s * t" for s t :: real\) vps + in foldr1 (fn (s, t) => \<^instantiate>\s and t in cterm \s * t\ for s t :: real\) vps end fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c else if c = @1 then cterm_of_monomial m - else \<^instantiate>\x = \cterm_of_rat c\ and y = \cterm_of_monomial m\ in cterm "x * y" for x y :: real\; + else \<^instantiate>\x = \cterm_of_rat c\ and y = \cterm_of_monomial m\ in cterm \x * y\ for x y :: real\; fun cterm_of_poly p = if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\0::real\ @@ -345,7 +345,7 @@ let val cms = map cterm_of_cmonomial (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p)) - in foldr1 (fn (t1, t2) => \<^instantiate>\t1 and t2 in cterm "t1 + t2" for t1 t2 :: real\) cms + in foldr1 (fn (t1, t2) => \<^instantiate>\t1 and t2 in cterm \t1 + t2\ for t1 t2 :: real\) cms end; (* A general real arithmetic prover *) @@ -405,13 +405,13 @@ | Axiom_lt n => nth lts n | Rational_eq x => eqT_elim (numeric_eq_conv - \<^instantiate>\x = \mk_numeric x\ in cprop "x = 0" for x :: real\) + \<^instantiate>\x = \mk_numeric x\ in cprop \x = 0\ for x :: real\) | Rational_le x => eqT_elim (numeric_ge_conv - \<^instantiate>\x = \mk_numeric x\ in cprop "x \ 0" for x :: real\) + \<^instantiate>\x = \mk_numeric x\ in cprop \x \ 0\ for x :: real\) | Rational_lt x => eqT_elim (numeric_gt_conv - \<^instantiate>\x = \mk_numeric x\ in cprop "x > 0" for x :: real\) + \<^instantiate>\x = \mk_numeric x\ in cprop \x > 0\ for x :: real\) | Square pt => square_rule (cterm_of_poly pt) | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p) | Sum(p1,p2) => add_rule (translate p1) (translate p2) @@ -519,7 +519,7 @@ fun mk_ex v t = \<^instantiate>\'a = \Thm.ctyp_of_cterm v\ and P = \Thm.lambda v t\ - in cprop "Ex P" for P :: "'a \ bool"\ + in cprop \Ex P\ for P :: \'a \ bool\\ fun choose v th th' = case Thm.concl_of th of @@ -560,7 +560,7 @@ fun absremover ct = (literals_conv [\<^term>\HOL.conj\, \<^term>\HOL.disj\] [] (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct - val nct = \<^instantiate>\ct in cprop "\ ct"\ + val nct = \<^instantiate>\A = ct in cprop \\ A\\ val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct val tm0 = Thm.dest_arg (Thm.rhs_of th0) val (th, certificates) = diff -r 0eb2f18b1806 -r c14787d73db6 src/HOL/ex/Sorting_Algorithms_Examples.thy --- a/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 21:46:38 2021 +0200 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 21:58:11 2021 +0200 @@ -25,7 +25,7 @@ fun raw_sort (ctxt, ct, ks) = \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt (term_of_int_list ks)\ - in cterm "x \ y" for x y :: "int list"\; + in cterm \x \ y\ for x y :: \int list\\; val (_, sort_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\sort\, raw_sort)));