# HG changeset patch
# User wenzelm
# Date 1527800217 -7200
# Node ID 70818e1bb1511563aa662fc425973faabcb1fe7d
# Parent  09ac56914b299d5d6657a113888bd2dbd9413101
more symbols;

diff -r 09ac56914b29 -r 70818e1bb151 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu May 31 22:27:13 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu May 31 22:56:57 2018 +0200
@@ -92,13 +92,13 @@
   end;
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_open_vcg}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
     "open a new SPARK environment and load a SPARK-generated .vcg file"
     (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_open}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_open\<close>
     "open a new SPARK environment and load a SPARK-generated .siv file"
     (Resources.provide_parse_files "spark_open" -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
@@ -107,13 +107,13 @@
   (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_proof_functions}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_proof_functions\<close>
     "associate SPARK proof functions with terms"
     (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
       (Toplevel.theory o fold add_proof_fun_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_types}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_types\<close>
     "associate SPARK types with types"
     (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
        Scan.optional (Args.parens (Parse.list1
@@ -121,12 +121,12 @@
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>spark_vc\<close>
     "enter into proof mode for a specific verification condition"
     (Parse.name >> prove_vc);
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_status}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_status\<close>
     "show the name and state of all loaded verification conditions"
     (Scan.optional
        (Args.parens
@@ -136,10 +136,10 @@
         Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
 
 val _ =
-  Outer_Syntax.command @{command_keyword spark_end}
+  Outer_Syntax.command \<^command_keyword>\<open>spark_end\<close>
     "close the current SPARK environment"
-    (Scan.optional (@{keyword "("} |-- Parse.!!!
-         (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
+    (Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!!
+         (Parse.reserved "incomplete" --| \<^keyword>\<open>)\<close>) >> K true) false >>
        (Toplevel.theory o SPARK_VCs.close));
 
 val _ = Theory.setup (Theory.at_end (fn thy =>
diff -r 09ac56914b29 -r 70818e1bb151 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu May 31 22:27:13 2018 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu May 31 22:56:57 2018 +0200
@@ -101,7 +101,7 @@
     val T = HOLogic.dest_setT setT;
     val U = HOLogic.dest_setT (fastype_of u)
   in
-    Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) -->
+    Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
       HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
   end;
 
@@ -150,7 +150,7 @@
   in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
 
 fun get_record_info thy T = (case Record.dest_recTs T of
-    [(tyname, [@{typ unit}])] =>
+    [(tyname, [\<^typ>\<open>unit\<close>])] =>
       Record.get_info thy (Long_Name.qualifier tyname)
   | _ => NONE);
 
@@ -177,9 +177,9 @@
     val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
-    val p = Const (@{const_name pos}, T --> HOLogic.intT);
-    val v = Const (@{const_name val}, HOLogic.intT --> T);
-    val card = Const (@{const_name card},
+    val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
+    val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
+    val card = Const (\<^const_name>\<open>card\<close>,
       HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
 
     fun mk_binrel_def s f = Logic.mk_equals
@@ -190,7 +190,7 @@
 
     val (((def1, def2), def3), lthy) = thy |>
 
-      Class.instantiation ([tyname'], [], @{sort spark_enum}) |>
+      Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>
 
       define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
         (p,
@@ -199,9 +199,9 @@
            map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
 
       define_overloaded ("less_eq_" ^ tyname ^ "_def",
-        mk_binrel_def @{const_name less_eq} p) ||>>
+        mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
       define_overloaded ("less_" ^ tyname ^ "_def",
-        mk_binrel_def @{const_name less} p);
+        mk_binrel_def \<^const_name>\<open>less\<close> p);
 
     val UNIV_eq = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -214,7 +214,7 @@
          ALLGOALS (asm_full_simp_tac ctxt));
 
     val finite_UNIV = Goal.prove lthy [] []
-      (HOLogic.mk_Trueprop (Const (@{const_name finite},
+      (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
          HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
 
@@ -225,13 +225,13 @@
 
     val range_pos = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name image}, (T --> HOLogic.intT) -->
+         (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
             HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
               p $ HOLogic.mk_UNIV T,
-          Const (@{const_name atLeastLessThan}, HOLogic.intT -->
+          Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
             HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
               HOLogic.mk_number HOLogic.intT 0 $
-              (@{term int} $ card))))
+              (\<^term>\<open>int\<close> $ card))))
       (fn {context = ctxt, ...} =>
          simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
          simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
@@ -264,12 +264,12 @@
 
     val first_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name first_el}, T), hd cs)))
+         (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
 
     val last_el = Goal.prove lthy' [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (@{const_name last_el}, T), List.last cs)))
+         (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
       (fn {context = ctxt, ...} =>
         simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   in
@@ -414,43 +414,43 @@
       | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
 
-      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+      | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
 
-      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
+      | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
 
-      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+      | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
 
-      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
+      | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
 
-      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus}
+      | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop @{const_name minus}
+      | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times}
+      | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide}
+      | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
+      | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo}
+      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
       | tm_of vs (Funct ("-", [e])) =
-          (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
+          (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
 
       | tm_of vs (Funct ("**", [e, e'])) =
-          (Const (@{const_name power}, HOLogic.intT --> HOLogic.natT -->
+          (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
              HOLogic.intT) $ fst (tm_of vs e) $
-               (@{const nat} $ fst (tm_of vs e')), integerN)
+               (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
 
       | tm_of (tab, _) (Ident s) =
           (case Symtab.lookup tab s of
@@ -528,7 +528,7 @@
           (* enumeration type to integer *)
           (case try (unsuffix "__pos") s of
              SOME tyname => (case es of
-               [e] => (Const (@{const_name pos},
+               [e] => (Const (\<^const_name>\<open>pos\<close>,
                    mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
                  integerN)
              | _ => error ("Function " ^ s ^ " expects one argument"))
@@ -537,7 +537,7 @@
           (* integer to enumeration type *)
           (case try (unsuffix "__val") s of
              SOME tyname => (case es of
-               [e] => (Const (@{const_name val},
+               [e] => (Const (\<^const_name>\<open>val\<close>,
                    HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
                  tyname)
              | _ => error ("Function " ^ s ^ " expects one argument"))
@@ -550,8 +550,8 @@
                   val (t, tyname) = tm_of vs e;
                   val T = mk_type thy prfx tyname
                 in (Const
-                  (if s = "succ" then @{const_name succ}
-                   else @{const_name pred}, T --> T) $ t, tyname)
+                  (if s = "succ" then \<^const_name>\<open>succ\<close>
+                   else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
                 end
             | _ => error ("Function " ^ s ^ " expects one argument"))
 
@@ -580,7 +580,7 @@
                   val U = mk_type thy prfx elty;
                   val fT = T --> U
                 in
-                  (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
+                  (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
                      t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
                        fst (tm_of vs e'),
                    ty)
@@ -628,7 +628,7 @@
                  val T = foldr1 HOLogic.mk_prodT Ts;
                  val U = mk_type thy prfx elty;
                  fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
-                   | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
+                   | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
                        T --> T --> HOLogic.mk_setT T) $
                          fst (tm_of vs e) $ fst (tm_of vs e');
                  fun mk_idx idx =
@@ -638,22 +638,22 @@
                  fun mk_upd (idxs, e) t =
                    if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
                    then
-                     Const (@{const_name fun_upd}, (T --> U) -->
+                     Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
                          T --> U --> T --> U) $ t $
                        foldl1 HOLogic.mk_prod
                          (map (fst o tm_of vs o fst) (hd idxs)) $
                        fst (tm_of vs e)
                    else
-                     Const (@{const_name fun_upds}, (T --> U) -->
+                     Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
                          HOLogic.mk_setT T --> U --> T --> U) $ t $
-                       foldl1 (HOLogic.mk_binop @{const_name sup})
+                       foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
                          (map mk_idx idxs) $
                        fst (tm_of vs e)
                in
                  (fold mk_upd assocs
                     (case default of
                        SOME e => Abs ("x", T, fst (tm_of vs e))
-                     | NONE => Const (@{const_name undefined}, T --> U)),
+                     | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
                   s)
                end
            | _ => error (s ^ " is not an array type"))
@@ -973,7 +973,7 @@
              \because their proofs contain oracles:" proved'));
           val prv_path = Path.ext "prv" path;
           val _ =
-            if File.exists prv_path orelse Options.default_bool @{system_option spark_prv} then
+            if File.exists prv_path orelse Options.default_bool \<^system_option>\<open>spark_prv\<close> then
               File.write prv_path
                (implode (map (fn (s, _) => snd (strip_number s) ^
                   " -- proved by " ^ Distribution.version ^ "\n") proved''))
@@ -1096,8 +1096,8 @@
 
     val (((defs', vars''), ivars), (ids, thy')) =
       ((Symtab.empty |>
-        Symtab.update ("false", (@{term False}, booleanN)) |>
-        Symtab.update ("true", (@{term True}, booleanN)),
+        Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
+        Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
         Name.context),
        thy |> Sign.add_path
          ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>