--- 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);
--- 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
*}
--- 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);
--- 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;
--- 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
--- 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)
);
--- 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);
--- 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) [] --
--- 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) [] --