# HG changeset patch
# User haftmann
# Date 1486502106 -3600
# Node ID d51478d6aae44fc1ef63c3adc78bc60656d2e90c
# Parent  067a6cca39f0f3dcfa81d66afe7bdeffa8356736
isabelle update_cartouches

diff -r 067a6cca39f0 -r d51478d6aae4 src/HOL/Decision_Procs/Algebra_Aux.thy
--- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Tue Feb 07 22:15:05 2017 +0100
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Tue Feb 07 22:15:06 2017 +0100
@@ -59,7 +59,7 @@
   show ?thesis
   proof (cases "0 \<le> j")
     case True
-    with `0 \<le> i` show ?thesis by (simp add: of_integer_def nat_add_distrib)
+    with \<open>0 \<le> i\<close> show ?thesis by (simp add: of_integer_def nat_add_distrib)
   next
     case False
     show ?thesis
@@ -67,19 +67,19 @@
       case True
       then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (i - (- j))\<guillemotright>\<^sub>\<nat>"
         by (simp add: of_integer_def)
-      also from True `0 \<le> i` `\<not> 0 \<le> j`
+      also from True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
       have "nat (i - (- j)) = nat i - nat (- j)"
         by (simp add: nat_diff_distrib)
-      finally show ?thesis using True `0 \<le> i` `\<not> 0 \<le> j`
+      finally show ?thesis using True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
         by (simp add: minus_eq of_integer_def)
     next
       case False
       then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- j - i)\<guillemotright>\<^sub>\<nat>"
         by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
-      also from False `0 \<le> i` `\<not> 0 \<le> j`
+      also from False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
       have "nat (- j - i) = nat (- j) - nat i"
         by (simp add: nat_diff_distrib)
-      finally show ?thesis using False `0 \<le> i` `\<not> 0 \<le> j`
+      finally show ?thesis using False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
         by (simp add: minus_eq minus_add a_ac of_integer_def)
     qed
   qed
@@ -93,24 +93,24 @@
       case True
       then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (j - (- i))\<guillemotright>\<^sub>\<nat>"
         by (simp add: of_integer_def add_ac)
-      also from True `\<not> 0 \<le> i` `0 \<le> j`
+      also from True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
       have "nat (j - (- i)) = nat j - nat (- i)"
         by (simp add: nat_diff_distrib)
-      finally show ?thesis using True `\<not> 0 \<le> i` `0 \<le> j`
+      finally show ?thesis using True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
         by (simp add: minus_eq minus_add a_ac of_integer_def)
     next
       case False
       then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- i - j)\<guillemotright>\<^sub>\<nat>"
         by (simp add: of_integer_def)
-      also from False `\<not> 0 \<le> i` `0 \<le> j`
+      also from False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
       have "nat (- i - j) = nat (- i) - nat j"
         by (simp add: nat_diff_distrib)
-      finally show ?thesis using False `\<not> 0 \<le> i` `0 \<le> j`
+      finally show ?thesis using False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
         by (simp add: minus_eq minus_add of_integer_def)
     qed
   next
     case False
-    with `\<not> 0 \<le> i` show ?thesis
+    with \<open>\<not> 0 \<le> i\<close> show ?thesis
       by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
         del: add_uminus_conv_diff uminus_add_conv_diff)
   qed
@@ -128,11 +128,11 @@
   show ?thesis
   proof (cases "0 \<le> j")
     case True
-    with `0 \<le> i` show ?thesis
+    with \<open>0 \<le> i\<close> show ?thesis
       by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
   next
     case False
-    with `0 \<le> i` show ?thesis
+    with \<open>0 \<le> i\<close> show ?thesis
       by (simp add: of_integer_def zero_le_mult_iff
         minus_mult_right nat_mult_distrib r_minus
         del: minus_mult_right [symmetric])
@@ -142,13 +142,13 @@
   show ?thesis
   proof (cases "0 \<le> j")
     case True
-    with `\<not> 0 \<le> i` show ?thesis
+    with \<open>\<not> 0 \<le> i\<close> show ?thesis
       by (simp add: of_integer_def zero_le_mult_iff
         minus_mult_left nat_mult_distrib l_minus
         del: minus_mult_left [symmetric])
   next
     case False
-    with `\<not> 0 \<le> i` show ?thesis
+    with \<open>\<not> 0 \<le> i\<close> show ?thesis
       by (simp add: of_integer_def zero_le_mult_iff
         minus_mult_minus [of i j, symmetric] nat_mult_distrib
         l_minus r_minus
diff -r 067a6cca39f0 -r d51478d6aae4 src/HOL/Decision_Procs/Conversions.thy
--- a/src/HOL/Decision_Procs/Conversions.thy	Tue Feb 07 22:15:05 2017 +0100
+++ b/src/HOL/Decision_Procs/Conversions.thy	Tue Feb 07 22:15:06 2017 +0100
@@ -6,24 +6,24 @@
 imports Main
 begin
 
-ML {*
+ML \<open>
 fun tactic_of_conv cv i st =
   if i > Thm.nprems_of st then Seq.empty
   else Seq.single (Conv.gconv_rule cv i st);
 
 fun binop_conv cv cv' = Conv.combination_conv (Conv.arg_conv cv) cv';
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun err s ct =
    error (s ^ ": " ^ Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct));
-*}
+\<close>
 
 attribute_setup meta =
-  {* Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th))) *}
-  {* convert equality to meta equality *}
+  \<open>Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th)))\<close>
+  \<open>convert equality to meta equality\<close>
 
-ML {*
+ML \<open>
 fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
 
 fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
@@ -77,20 +77,20 @@
 
 fun args1 conv ct = conv (Thm.dest_arg ct);
 fun args2 conv ct = conv (Thm.dest_arg1 ct) (Thm.dest_arg ct);
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun strip_numeral ct = (case strip_app ct of
     (@{const_name uminus}, [n]) => (case strip_app n of
       (@{const_name numeral}, [b]) => (@{const_name uminus}, [b])
     | _ => ("", []))
   | x => x);
-*}
+\<close>
 
 lemma nat_minus1_eq: "nat (- 1) = 0"
   by simp
 
-ML {*
+ML \<open>
 fun nat_conv i = (case strip_app i of
     (@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
   | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
@@ -98,9 +98,9 @@
   | (@{const_name uminus}, [b]) => (case strip_app b of
       (@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
     | (@{const_name numeral}, [b']) => inst [] [b'] @{thm nat_neg_numeral [meta]}));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun add_num_conv b b' = (case (strip_app b, strip_app b') of
     ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
       @{thm add_num_simps(1) [meta]}
@@ -132,9 +132,9 @@
       transitive'
         (inst [] [m, n] @{thm add_num_simps(9) [meta]})
         (cong1 (cong2' add_num_conv (args2 add_num_conv) Thm.reflexive)));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun BitM_conv m = (case strip_app m of
     (@{const_name Num.One}, []) => @{thm BitM.simps(1) [meta]}
   | (@{const_name Num.Bit0}, [n]) =>
@@ -143,13 +143,13 @@
         (cong1 (args1 BitM_conv))
   | (@{const_name Num.Bit1}, [n]) =>
       inst [] [n] @{thm BitM.simps(3) [meta]});
-*}
+\<close>
 
 lemma dbl_neg_numeral:
   "Num.dbl (- Num.numeral k) = - Num.numeral (Num.Bit0 k)"
   by simp
 
-ML {*
+ML \<open>
 fun dbl_conv a =
   let
     val dbl_neg_numeral_a = inst [a] [] @{thm dbl_neg_numeral [meta]};
@@ -162,13 +162,13 @@
       | (@{const_name numeral}, [k]) => inst [] [k] dbl_numeral_a
       | (@{const_name uminus}, [k]) => inst [] [k] dbl_neg_numeral_a
   end;
-*}
+\<close>
 
 lemma dbl_inc_neg_numeral:
   "Num.dbl_inc (- Num.numeral k) = - Num.numeral (Num.BitM k)"
   by simp
 
-ML {*
+ML \<open>
 fun dbl_inc_conv a =
   let
     val dbl_inc_neg_numeral_a = inst [a] [] @{thm dbl_inc_neg_numeral [meta]};
@@ -184,13 +184,13 @@
             (inst [] [k] dbl_inc_neg_numeral_a)
             (cong1 (cong1 (args1 BitM_conv)))
   end;
-*}
+\<close>
 
 lemma dbl_dec_neg_numeral:
   "Num.dbl_dec (- Num.numeral k) = - Num.numeral (Num.Bit1 k)"
   by simp
 
-ML {*
+ML \<open>
 fun dbl_dec_conv a =
   let
     val dbl_dec_neg_numeral_a = inst [a] [] @{thm dbl_dec_neg_numeral [meta]};
@@ -206,9 +206,9 @@
             (inst [] [k] dbl_dec_numeral_a)
             (cong1 (args1 BitM_conv))
   end;
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun sub_conv a =
   let
     val [sub_One_One, sub_One_Bit0, sub_One_Bit1,
@@ -251,9 +251,9 @@
             (inst [] [k, l] sub_Bit1_Bit1)
             (cong1' dbl_conv_a (args2 conv)))
   in conv end;
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun expand1 a =
   let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta, symmetric]}
   in
@@ -283,9 +283,9 @@
                  numeral_1_eq_1_a)
       | _ => eq
   end;
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun plus_conv f a =
   let
     val add_0_a = inst [a] [] @{thm add_0 [meta]};
@@ -304,13 +304,13 @@
   in f conv end;
 
 val nat_plus_conv = plus_conv I @{ctyp nat};
-*}
+\<close>
 
 lemma neg_numeral_plus_neg_numeral:
   "- Num.numeral m + - Num.numeral n = (- Num.numeral (m + n) ::'a::neg_numeral)"
   by simp
 
-ML {*
+ML \<open>
 fun plus_neg_conv a =
   let
     val numeral_plus_neg_numeral_a =
@@ -341,12 +341,12 @@
 fun plus_conv' a = norm1_eq a oo plus_conv (plus_neg_conv a) a;
 
 val int_plus_conv = plus_conv' @{ctyp int};
-*}
+\<close>
 
 lemma minus_one: "- 1 = - 1" by simp
 lemma minus_numeral: "- numeral b = - numeral b" by simp
 
-ML {*
+ML \<open>
 fun uminus_conv a =
   let
     val minus_zero_a = inst [a] [] @{thm minus_zero [meta]};
@@ -363,9 +363,9 @@
   end;
 
 val int_neg_conv = uminus_conv @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun minus_conv a =
   let
     val [numeral_minus_numeral_a, numeral_minus_neg_numeral_a,
@@ -402,9 +402,9 @@
   in norm1_eq_a oo conv end;
 
 val int_minus_conv = minus_conv @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 val int_numeral = Thm.apply @{cterm "numeral :: num \<Rightarrow> int"};
 
 val nat_minus_refl = Thm.reflexive @{cterm "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"};
@@ -421,9 +421,9 @@
         (inst [] [m, n] @{thm diff_nat_numeral [meta]})
         (cong1' nat_conv (args2 int_minus_conv))
   | _ => cong2'' nat_minus_conv (expand1_nat m) (expand1_nat n));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun mult_num_conv m n = (case (strip_app m, strip_app n) of
     (_, (@{const_name Num.One}, [])) =>
       inst [] [m] @{thm mult_num_simps(1) [meta]}
@@ -447,9 +447,9 @@
         (cong1 (cong2' add_num_conv
            (args2 add_num_conv)
            (cong1 (args2 mult_num_conv)))));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun mult_conv f a =
   let
     val mult_zero_left_a = inst [a] [] @{thm mult_zero_left [meta]};
@@ -469,9 +469,9 @@
   in norm1_eq_a oo f conv end;
 
 val nat_mult_conv = mult_conv I @{ctyp nat};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun mult_neg_conv a =
   let
     val [neg_numeral_times_neg_numeral_a, neg_numeral_times_numeral_a,
@@ -498,9 +498,9 @@
 fun mult_conv' a = mult_conv (mult_neg_conv a) a;
 
 val int_mult_conv = mult_conv' @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun eq_num_conv m n = (case (strip_app m, strip_app n) of
     ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
       @{thm eq_num_simps(1) [meta]}
@@ -524,9 +524,9 @@
       Thm.transitive
         (inst [] [m, n] @{thm eq_num_simps(9) [meta]})
         (eq_num_conv m n));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun eq_conv f a =
   let
     val zero_eq_zero_a = inst [a] [] @{thm refl [of 0, THEN Eq_TrueI]};
@@ -552,9 +552,9 @@
   in f conv end;
 
 val nat_eq_conv = eq_conv I @{ctyp nat};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun eq_neg_conv a =
   let
     val neg_numeral_neq_zero_a =
@@ -587,9 +587,9 @@
 fun eq_conv' a = eq_conv (eq_neg_conv a) a;
 
 val int_eq_conv = eq_conv' @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun le_num_conv m n = (case (strip_app m, strip_app n) of
     ((@{const_name Num.One}, []), _) =>
       inst [] [n] @{thm le_num_simps(1) [meta]}
@@ -637,9 +637,9 @@
       Thm.transitive
         (inst [] [m, n] @{thm less_num_simps(7) [meta]})
         (less_num_conv m n));
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun le_conv f a =
   let
     val zero_le_zero_a = inst [a] [] @{thm order_refl [of 0, THEN Eq_TrueI]};
@@ -665,9 +665,9 @@
   in f conv end;
 
 val nat_le_conv = le_conv I @{ctyp nat};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun le_neg_conv a =
   let
     val neg_numeral_le_zero_a =
@@ -700,9 +700,9 @@
 fun le_conv' a = le_conv (le_neg_conv a) a;
 
 val int_le_conv = le_conv' @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun less_conv f a =
   let
     val not_zero_less_zero_a = inst [a] [] @{thm less_irrefl [of 0, THEN Eq_FalseI]};
@@ -728,9 +728,9 @@
   in f conv end;
 
 val nat_less_conv = less_conv I @{ctyp nat};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun less_neg_conv a =
   let
     val neg_numeral_less_zero_a =
@@ -763,9 +763,9 @@
 fun less_conv' a = less_conv (less_neg_conv a) a;
 
 val int_less_conv = less_conv' @{ctyp int};
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun If_conv a =
   let
     val if_True = inst [a] [] @{thm if_True [meta]};
@@ -804,9 +804,9 @@
             | _ => err "If_conv" (Thm.rhs_of p_eq)
           end
   end;
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun drop_conv a =
   let
     val drop_0_a = inst [a] [] @{thm drop_0 [meta]};
@@ -823,9 +823,9 @@
                  Thm.reflexive
                  (cong2' conv (args2 nat_minus_conv) Thm.reflexive))))
   in conv end;
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun nth_conv a =
   let
     val nth_Cons_a = inst [a] [] @{thm nth_Cons' [meta]};
@@ -839,6 +839,6 @@
                Thm.reflexive
                (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
   in conv end;
-*}
+\<close>
 
 end
diff -r 067a6cca39f0 -r d51478d6aae4 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Feb 07 22:15:05 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Feb 07 22:15:06 2017 +0100
@@ -597,14 +597,14 @@
   then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R"
     "peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)"
     by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm)
-  from `in_carrier xs` `nonzero xs (Cond e2)`
+  from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
   have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
     by (rule fnorm_correct)
-  moreover from `in_carrier xs` `nonzero xs (Cond e2)`
+  moreover from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
   have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
-  ultimately have "feval xs e2 \<noteq> \<zero>" using `peval xs (Num e2) \<noteq> \<zero>` `in_carrier xs`
+  ultimately have "feval xs e2 \<noteq> \<zero>" using \<open>peval xs (Num e2) \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
     by (simp add: divide_eq_0_iff)
-  with `feval xs e1 \<in> carrier R` `feval xs e2 \<in> carrier R`
+  with \<open>feval xs e1 \<in> carrier R\<close> \<open>feval xs e2 \<in> carrier R\<close>
   show ?case by simp
 qed (simp_all add: nonzero_union split: prod.split_asm)
 
@@ -623,17 +623,17 @@
   show ?thesis
   proof
     assume "feval xs e = feval xs e'"
-    with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d`
-      `in_carrier xs` `nonzero xs (Cond e')`
+    with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close>
+      \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e')\<close>
     have "peval xs n \<oslash> peval xs d = \<zero>"
       by (simp add: fexpr_in_carrier minus_eq r_neg)
-    with `peval xs d \<noteq> \<zero>` `in_carrier xs`
+    with \<open>peval xs d \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
     show "peval xs n = \<zero>"
       by (simp add: divide_eq_0_iff)
   next
     assume "peval xs n = \<zero>"
-    with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` `peval xs d \<noteq> \<zero>`
-      `nonzero xs (Cond e)` `nonzero xs (Cond e')` `in_carrier xs`
+    with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close> \<open>peval xs d \<noteq> \<zero>\<close>
+      \<open>nonzero xs (Cond e)\<close> \<open>nonzero xs (Cond e')\<close> \<open>in_carrier xs\<close>
     show "feval xs e = feval xs e'"
       by (simp add: eq_diff0 fexpr_in_carrier)
   qed
@@ -652,7 +652,7 @@
 definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where
   "field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)"
 
-ML {*
+ML \<open>
 signature FIELD_TAC =
 sig
   structure Field_Simps:
@@ -916,11 +916,11 @@
     end);
 
 end
-*}
+\<close>
 
 context field begin
 
-local_setup {*
+local_setup \<open>
 Local_Theory.declaration {syntax = false, pervasive = false}
   (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
     (Morphism.term phi @{term R},
@@ -929,13 +929,13 @@
       Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
       singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
       singleton (Morphism.fact phi) @{thm feval_eq}))))
-*}
+\<close>
 
 end
 
-method_setup field = {*
+method_setup field = \<open>
   Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt =>
     SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt))
-*} "reduce equations over fields to equations over rings"
+\<close> "reduce equations over fields to equations over rings"
 
 end