avoid redundant escaping of Isabelle symbols;
authorwenzelm
Sat Jan 26 20:01:37 2008 +0100 (2008-01-26)
changeset 259858d69087f6a4b
parent 25984 da0399c9ffcb
child 25986 26f1e4c172c3
avoid redundant escaping of Isabelle symbols;
doc-src/AxClass/Nat/NatClass.ML
src/HOL/Library/Eval.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/ex/coopertac.ML
src/Tools/code/code_target.ML
src/Tools/induct.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 17:08:43 2008 +0100
     1.2 +++ b/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 20:01:37 2008 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  back();
     1.5  back();
     1.6  
     1.7 -Goalw [add_def] "\\<zero>+n = n";
     1.8 +Goalw [add_def] "\<zero>+n = n";
     1.9  by (rtac rec_0 1);
    1.10  qed "add_0";
    1.11  
    1.12 @@ -50,7 +50,7 @@
    1.13  by (Asm_simp_tac 1);
    1.14  qed "add_assoc";
    1.15  
    1.16 -Goal "m+\\<zero> = m";
    1.17 +Goal "m+\<zero> = m";
    1.18  by (res_inst_tac [("n","m")] induct 1);
    1.19  by (Simp_tac 1);
    1.20  by (Asm_simp_tac 1);
     2.1 --- a/src/HOL/Library/Eval.thy	Sat Jan 26 17:08:43 2008 +0100
     2.2 +++ b/src/HOL/Library/Eval.thy	Sat Jan 26 20:01:37 2008 +0100
     2.3 @@ -39,9 +39,9 @@
     2.4    fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
     2.5      | Fun_tr ts = raise TERM("Fun_tr", ts);
     2.6  in [
     2.7 -  ("\\<^fixed>pure_term_Type", Type_tr),
     2.8 -  ("\\<^fixed>pure_term_TFree", TFree_tr),
     2.9 -  ("\\<^fixed>pure_term_Fun", Fun_tr)
    2.10 +  ("\<^fixed>pure_term_Type", Type_tr),
    2.11 +  ("\<^fixed>pure_term_TFree", TFree_tr),
    2.12 +  ("\<^fixed>pure_term_Fun", Fun_tr)
    2.13  ] end
    2.14  *}
    2.15  
     3.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 26 17:08:43 2008 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jan 26 20:01:37 2008 +0100
     3.3 @@ -129,7 +129,7 @@
     3.4  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
     3.5  
     3.6  val def_inst =
     3.7 -  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
     3.8 +  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
     3.9        -- Args.term) >> SOME ||
    3.10      inst >> Option.map (pair NONE);
    3.11  
     4.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 17:08:43 2008 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 20:01:37 2008 +0100
     4.3 @@ -153,7 +153,7 @@
     4.4    | perm_simproc' thy ss _ = NONE;
     4.5  
     4.6  val perm_simproc =
     4.7 -  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \\<bullet> (pi2 \\<bullet> x)"] perm_simproc';
     4.8 +  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
     4.9  
    4.10  val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE;
    4.11  
     5.1 --- a/src/HOL/ex/coopertac.ML	Sat Jan 26 17:08:43 2008 +0100
     5.2 +++ b/src/HOL/ex/coopertac.ML	Sat Jan 26 20:01:37 2008 +0100
     5.3 @@ -36,7 +36,7 @@
     5.4  val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
     5.5  
     5.6  (*
     5.7 -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"]);
     5.8 +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"]);
     5.9  *)
    5.10  fun prepare_for_linz q fm = 
    5.11    let
     6.1 --- a/src/Tools/code/code_target.ML	Sat Jan 26 17:08:43 2008 +0100
     6.2 +++ b/src/Tools/code/code_target.ML	Sat Jan 26 20:01:37 2008 +0100
     6.3 @@ -2132,7 +2132,7 @@
     6.4    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
     6.5      parse_multi_syntax P.xname
     6.6        (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
     6.7 -        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
     6.8 +        (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
     6.9      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    6.10            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
    6.11    );
     7.1 --- a/src/Tools/induct.ML	Sat Jan 26 17:08:43 2008 +0100
     7.2 +++ b/src/Tools/induct.ML	Sat Jan 26 20:01:37 2008 +0100
     7.3 @@ -714,7 +714,7 @@
     7.4  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
     7.5  
     7.6  val def_inst =
     7.7 -  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
     7.8 +  ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
     7.9        -- Args.term) >> SOME ||
    7.10      inst >> Option.map (pair NONE);
    7.11  
     8.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Jan 26 17:08:43 2008 +0100
     8.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 26 20:01:37 2008 +0100
     8.3 @@ -413,7 +413,7 @@
     8.4    >> P.triple1;
     8.5  
     8.6  val datatype_decl =
     8.7 -  (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
     8.8 +  (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
     8.9    P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
    8.10    Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
    8.11    Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
     9.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Jan 26 17:08:43 2008 +0100
     9.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 26 20:01:37 2008 +0100
     9.3 @@ -584,7 +584,7 @@
     9.4  
     9.5  val ind_decl =
     9.6    (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
     9.7 -      ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
     9.8 +      ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
     9.9    (P.$$$ "intros" |--
    9.10      P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
    9.11    Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --