# HG changeset patch
# User wenzelm
# Date 1201374097 -3600
# Node ID 8d69087f6a4b1c02864ad10b72ddb89539226640
# Parent  da0399c9ffcb59bb7bea558dda63078bef215f00
avoid redundant escaping of Isabelle symbols;

diff -r da0399c9ffcb -r 8d69087f6a4b doc-src/AxClass/Nat/NatClass.ML
--- a/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -34,7 +34,7 @@
 back();
 back();
 
-Goalw [add_def] "\\<zero>+n = n";
+Goalw [add_def] "\<zero>+n = n";
 by (rtac rec_0 1);
 qed "add_0";
 
@@ -50,7 +50,7 @@
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
-Goal "m+\\<zero> = m";
+Goal "m+\<zero> = m";
 by (res_inst_tac [("n","m")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
diff -r da0399c9ffcb -r 8d69087f6a4b src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Sat Jan 26 20:01:37 2008 +0100
@@ -39,9 +39,9 @@
   fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
     | Fun_tr ts = raise TERM("Fun_tr", ts);
 in [
-  ("\\<^fixed>pure_term_Type", Type_tr),
-  ("\\<^fixed>pure_term_TFree", TFree_tr),
-  ("\\<^fixed>pure_term_Fun", Fun_tr)
+  ("\<^fixed>pure_term_Type", Type_tr),
+  ("\<^fixed>pure_term_TFree", TFree_tr),
+  ("\<^fixed>pure_term_Fun", Fun_tr)
 ] end
 *}
 
diff -r da0399c9ffcb -r 8d69087f6a4b src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -129,7 +129,7 @@
 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
 
 val def_inst =
-  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
+  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
diff -r da0399c9ffcb -r 8d69087f6a4b src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -153,7 +153,7 @@
   | perm_simproc' thy ss _ = NONE;
 
 val perm_simproc =
-  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \\<bullet> (pi2 \\<bullet> x)"] perm_simproc';
+  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
 
 val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
 
diff -r da0399c9ffcb -r 8d69087f6a4b src/HOL/ex/coopertac.ML
--- a/src/HOL/ex/coopertac.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/HOL/ex/coopertac.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -36,7 +36,7 @@
 val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
 
 (*
-val fn_rews = List.concat (map thms ["allpairs.simps","iupt.simps","decr.simps", "decrnum.simps","disjuncts.simps","simpnum.simps", "simpfm.simps","numadd.simps","nummul.simps","numneg_def","numsub","simp_num_pair_def","not.simps","prep.simps","qelim.simps","minusinf.simps","plusinf.simps","rsplit0.simps","rlfm.simps","\\<Upsilon>.simps","\\<upsilon>.simps","linrqe_def", "ferrack_def", "Let_def", "numsub_def", "numneg_def","DJ_def", "imp_def", "evaldjf_def", "djf_def", "split_def", "eq_def", "disj_def", "simp_num_pair_def", "conj_def", "lt_def", "neq_def","gt_def"]);
+val fn_rews = List.concat (map thms ["allpairs.simps","iupt.simps","decr.simps", "decrnum.simps","disjuncts.simps","simpnum.simps", "simpfm.simps","numadd.simps","nummul.simps","numneg_def","numsub","simp_num_pair_def","not.simps","prep.simps","qelim.simps","minusinf.simps","plusinf.simps","rsplit0.simps","rlfm.simps","\<Upsilon>.simps","\<upsilon>.simps","linrqe_def", "ferrack_def", "Let_def", "numsub_def", "numneg_def","DJ_def", "imp_def", "evaldjf_def", "djf_def", "split_def", "eq_def", "disj_def", "simp_num_pair_def", "conj_def", "lt_def", "neq_def","gt_def"]);
 *)
 fun prepare_for_linz q fm = 
   let
diff -r da0399c9ffcb -r 8d69087f6a4b src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/Tools/code/code_target.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -2132,7 +2132,7 @@
   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
     parse_multi_syntax P.xname
       (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
-        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
+        (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
           fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   );
diff -r da0399c9ffcb -r 8d69087f6a4b src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/Tools/induct.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -714,7 +714,7 @@
 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
 
 val def_inst =
-  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
+  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
diff -r da0399c9ffcb -r 8d69087f6a4b src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -413,7 +413,7 @@
   >> P.triple1;
 
 val datatype_decl =
-  (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
+  (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
   Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
   Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
diff -r da0399c9ffcb -r 8d69087f6a4b src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -584,7 +584,7 @@
 
 val ind_decl =
   (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
-      ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
+      ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
   (P.$$$ "intros" |--
     P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
   Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --