eliminated ASCII syntax from Pure bootstrap;
authorwenzelm
Sun Feb 25 15:44:46 2018 +0100 (2018-02-25)
changeset 677215348bea4accd
parent 67718 17874d43d3b3
child 67722 012f1e8a1209
eliminated ASCII syntax from Pure bootstrap;
tuned comments;
src/Pure/Isar/local_defs.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/subgoal.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/simple_syntax.ML
src/Pure/Tools/find_theorems.ML
src/Pure/assumption.ML
src/Pure/conjunction.ML
src/Pure/conv.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/logic.ML
src/Pure/more_thm.ML
src/Pure/primitive_defs.ML
src/Pure/pure_thy.ML
src/Pure/raw_simplifier.ML
src/Pure/tactic.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun Feb 25 12:59:08 2018 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Feb 25 15:44:46 2018 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4  
     1.5  
     1.6  (*
     1.7 -  [x, x == a]
     1.8 +  [x, x \<equiv> a]
     1.9         :
    1.10        B x
    1.11    -----------
    1.12 @@ -133,7 +133,7 @@
    1.13  (* specific export -- result based on educated guessing *)
    1.14  
    1.15  (*
    1.16 -  [xs, xs == as]
    1.17 +  [xs, xs \<equiv> as]
    1.18          :
    1.19         B xs
    1.20    --------------
    1.21 @@ -158,11 +158,11 @@
    1.22    in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
    1.23  
    1.24  (*
    1.25 -  [xs, xs == as]
    1.26 +  [xs, xs \<equiv> as]
    1.27          :
    1.28       TERM b xs
    1.29    --------------  and  --------------
    1.30 -     TERM b as          b xs == b as
    1.31 +     TERM b as          b xs \<equiv> b as
    1.32  *)
    1.33  fun export_cterm inner outer ct =
    1.34    export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
     2.1 --- a/src/Pure/Isar/obtain.ML	Sun Feb 25 12:59:08 2018 +0100
     2.2 +++ b/src/Pure/Isar/obtain.ML	Sun Feb 25 15:44:46 2018 +0100
     2.3 @@ -144,11 +144,11 @@
     2.4  (** consider: generalized elimination and cases rule **)
     2.5  
     2.6  (*
     2.7 -  consider (a) x where "A x" | (b) y where "B y" | ... ==
     2.8 +  consider (a) x where "A x" | (b) y where "B y" | ... \<equiv>
     2.9  
    2.10    have thesis
    2.11 -    if a [intro?]: "!!x. A x ==> thesis"
    2.12 -    and b [intro?]: "!!y. B y ==> thesis"
    2.13 +    if a [intro?]: "\<And>x. A x \<Longrightarrow> thesis"
    2.14 +    and b [intro?]: "\<And>y. B y \<Longrightarrow> thesis"
    2.15      and ...
    2.16      for thesis
    2.17      apply (insert that)
    2.18 @@ -185,9 +185,9 @@
    2.19  (** obtain: augmented context based on generalized existence rule **)
    2.20  
    2.21  (*
    2.22 -  obtain (a) x where "A x" <proof> ==
    2.23 +  obtain (a) x where "A x" <proof> \<equiv>
    2.24  
    2.25 -  have thesis if a [intro?]: "!!x. A x ==> thesis" for thesis
    2.26 +  have thesis if a [intro?]: "\<And>x. A x \<Longrightarrow> thesis" for thesis
    2.27      apply (insert that)
    2.28      <proof>
    2.29    fix x assm <<obtain_export>> "A x"
    2.30 @@ -279,15 +279,15 @@
    2.31  
    2.32  (*
    2.33    <chain_facts>
    2.34 -  guess x <proof body> <proof end> ==
    2.35 +  guess x <proof body> <proof end> \<equiv>
    2.36  
    2.37    {
    2.38      fix thesis
    2.39      <chain_facts> have "PROP ?guess"
    2.40 -      apply magic      -- {* turn goal into "thesis ==> #thesis" *}
    2.41 +      apply magic      \<comment> \<open>turn goal into \<open>thesis \<Longrightarrow> #thesis\<close>\<close>
    2.42        <proof body>
    2.43 -      apply_end magic  -- {* turn final "(!!x. P x ==> thesis) ==> #thesis" into
    2.44 -        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
    2.45 +      apply_end magic  \<comment> \<open>turn final \<open>(\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> #thesis\<close> into\<close>
    2.46 +        \<comment> \<open>\<open>#((\<And>x. A x \<Longrightarrow> thesis) \<Longrightarrow> thesis)\<close> which is a finished goal state\<close>
    2.47        <proof end>
    2.48    }
    2.49    fix x assm <<obtain_export>> "A x"
     3.1 --- a/src/Pure/Isar/proof.ML	Sun Feb 25 12:59:08 2018 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Sun Feb 25 15:44:46 2018 +0100
     3.3 @@ -171,7 +171,7 @@
     3.4     {statement: (string * Position.T) * term list list * term,
     3.5        (*goal kind and statement (starting with vars), initial proposition*)
     3.6      using: thm list,                      (*goal facts*)
     3.7 -    goal: thm,                            (*subgoals ==> statement*)
     3.8 +    goal: thm,                            (*subgoals \<Longrightarrow> statement*)
     3.9      before_qed: Method.text option,
    3.10      after_qed:
    3.11        (context * thm list list -> state -> state) *
     4.1 --- a/src/Pure/Isar/subgoal.ML	Sun Feb 25 12:59:08 2018 +0100
     4.2 +++ b/src/Pure/Isar/subgoal.ML	Sun Feb 25 15:44:46 2018 +0100
     4.3 @@ -108,9 +108,9 @@
     4.4  (*
     4.5         [x, A x]
     4.6            :
     4.7 -       B x ==> C
     4.8 +       B x \<Longrightarrow> C
     4.9    ------------------
    4.10 -  [!!x. A x ==> B x]
    4.11 +  [\<And>x. A x \<Longrightarrow> B x]
    4.12            :
    4.13            C
    4.14  *)
     5.1 --- a/src/Pure/Proof/extraction.ML	Sun Feb 25 12:59:08 2018 +0100
     5.2 +++ b/src/Pure/Proof/extraction.ML	Sun Feb 25 15:44:46 2018 +0100
     5.3 @@ -40,10 +40,10 @@
     5.4      [(Binding.make ("Type", \<^here>), 0, NoSyn),
     5.5       (Binding.make ("Null", \<^here>), 0, NoSyn)]
     5.6    #> Sign.add_consts
     5.7 -    [(Binding.make ("typeof", \<^here>), typ "'b => Type", NoSyn),
     5.8 -     (Binding.make ("Type", \<^here>), typ "'a itself => Type", NoSyn),
     5.9 +    [(Binding.make ("typeof", \<^here>), typ "'b \<Rightarrow> Type", NoSyn),
    5.10 +     (Binding.make ("Type", \<^here>), typ "'a itself \<Rightarrow> Type", NoSyn),
    5.11       (Binding.make ("Null", \<^here>), typ "Null", NoSyn),
    5.12 -     (Binding.make ("realizes", \<^here>), typ "'a => 'b => 'b", NoSyn)];
    5.13 +     (Binding.make ("realizes", \<^here>), typ "'a \<Rightarrow> 'b \<Rightarrow> 'b", NoSyn)];
    5.14  
    5.15  val nullT = Type ("Null", []);
    5.16  val nullt = Const ("Null", nullT);
    5.17 @@ -430,45 +430,45 @@
    5.18    (add_types [("prop", ([], NONE))] #>
    5.19  
    5.20     add_typeof_eqns
    5.21 -     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
    5.22 -    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
    5.23 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))",
    5.24 +     ["(typeof (PROP P)) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>  \
    5.25 +    \  (typeof (PROP Q)) \<equiv> (Type (TYPE('Q))) \<Longrightarrow>  \
    5.26 +    \    (typeof (PROP P \<Longrightarrow> PROP Q)) \<equiv> (Type (TYPE('Q)))",
    5.27  
    5.28 -      "(typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
    5.29 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE(Null)))",
    5.30 +      "(typeof (PROP Q)) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>  \
    5.31 +    \    (typeof (PROP P \<Longrightarrow> PROP Q)) \<equiv> (Type (TYPE(Null)))",
    5.32  
    5.33 -      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
    5.34 -    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
    5.35 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('P => 'Q)))",
    5.36 +      "(typeof (PROP P)) \<equiv> (Type (TYPE('P))) \<Longrightarrow>  \
    5.37 +    \  (typeof (PROP Q)) \<equiv> (Type (TYPE('Q))) \<Longrightarrow>  \
    5.38 +    \    (typeof (PROP P \<Longrightarrow> PROP Q)) \<equiv> (Type (TYPE('P \<Rightarrow> 'Q)))",
    5.39  
    5.40 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
    5.41 -    \    (typeof (!!x. PROP P (x))) == (Type (TYPE(Null)))",
    5.42 +      "(\<lambda>x. typeof (PROP P (x))) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>  \
    5.43 +    \    (typeof (\<And>x. PROP P (x))) \<equiv> (Type (TYPE(Null)))",
    5.44  
    5.45 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==>  \
    5.46 -    \    (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
    5.47 +      "(\<lambda>x. typeof (PROP P (x))) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow>  \
    5.48 +    \    (typeof (\<And>x::'a. PROP P (x))) \<equiv> (Type (TYPE('a \<Rightarrow> 'P)))",
    5.49  
    5.50 -      "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==>  \
    5.51 -    \    (typeof (f)) == (Type (TYPE('f)))"] #>
    5.52 +      "(\<lambda>x. typeof (f (x))) \<equiv> (\<lambda>x. Type (TYPE('f))) \<Longrightarrow>  \
    5.53 +    \    (typeof (f)) \<equiv> (Type (TYPE('f)))"] #>
    5.54  
    5.55     add_realizes_eqns
    5.56 -     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
    5.57 -    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
    5.58 -    \    (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))",
    5.59 +     ["(typeof (PROP P)) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>  \
    5.60 +    \    (realizes (r) (PROP P \<Longrightarrow> PROP Q)) \<equiv>  \
    5.61 +    \    (PROP realizes (Null) (PROP P) \<Longrightarrow> PROP realizes (r) (PROP Q))",
    5.62  
    5.63 -      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
    5.64 -    \  (typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
    5.65 -    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
    5.66 -    \    (!!x::'P. PROP realizes (x) (PROP P) ==> PROP realizes (Null) (PROP Q))",
    5.67 +      "(typeof (PROP P)) \<equiv> (Type (TYPE('P))) \<Longrightarrow>  \
    5.68 +    \  (typeof (PROP Q)) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>  \
    5.69 +    \    (realizes (r) (PROP P \<Longrightarrow> PROP Q)) \<equiv>  \
    5.70 +    \    (\<And>x::'P. PROP realizes (x) (PROP P) \<Longrightarrow> PROP realizes (Null) (PROP Q))",
    5.71  
    5.72 -      "(realizes (r) (PROP P ==> PROP Q)) ==  \
    5.73 -    \  (!!x. PROP realizes (x) (PROP P) ==> PROP realizes (r (x)) (PROP Q))",
    5.74 +      "(realizes (r) (PROP P \<Longrightarrow> PROP Q)) \<equiv>  \
    5.75 +    \  (\<And>x. PROP realizes (x) (PROP P) \<Longrightarrow> PROP realizes (r (x)) (PROP Q))",
    5.76  
    5.77 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
    5.78 -    \    (realizes (r) (!!x. PROP P (x))) ==  \
    5.79 -    \    (!!x. PROP realizes (Null) (PROP P (x)))",
    5.80 +      "(\<lambda>x. typeof (PROP P (x))) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>  \
    5.81 +    \    (realizes (r) (\<And>x. PROP P (x))) \<equiv>  \
    5.82 +    \    (\<And>x. PROP realizes (Null) (PROP P (x)))",
    5.83  
    5.84 -      "(realizes (r) (!!x. PROP P (x))) ==  \
    5.85 -    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    5.86 +      "(realizes (r) (\<And>x. PROP P (x))) \<equiv>  \
    5.87 +    \  (\<And>x. PROP realizes (r (x)) (PROP P (x)))"] #>
    5.88  
    5.89     Attrib.setup \<^binding>\<open>extraction_expand\<close> (Scan.succeed (extraction_expand false))
    5.90       "specify theorems to be expanded during extraction" #>
     6.1 --- a/src/Pure/Syntax/simple_syntax.ML	Sun Feb 25 12:59:08 2018 +0100
     6.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Sun Feb 25 15:44:46 2018 +0100
     6.3 @@ -17,7 +17,7 @@
     6.4  (* scanning tokens *)
     6.5  
     6.6  val lexicon = Scan.make_lexicon
     6.7 -  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=>", "&&&", "CONST"]);
     6.8 +  (map Symbol.explode ["\<And>", "\<lambda>", "(", ")", ".", "::", "\<equiv>", "\<Longrightarrow>", "\<Rightarrow>", "&&&", "CONST"]);
     6.9  
    6.10  fun read scan s =
    6.11    (case
    6.12 @@ -53,7 +53,7 @@
    6.13  (* types *)
    6.14  
    6.15  (*
    6.16 -  typ  = typ1 => ... => typ1
    6.17 +  typ  = typ1 \<Rightarrow> ... \<Rightarrow> typ1
    6.18         | typ1
    6.19    typ1 = typ2 const ... const
    6.20         | typ2
    6.21 @@ -63,7 +63,7 @@
    6.22  *)
    6.23  
    6.24  fun typ x =
    6.25 - (enum1 "=>" typ1 >> (op ---> o split_last)) x
    6.26 + (enum1 "\<Rightarrow>" typ1 >> (op ---> o split_last)) x
    6.27  and typ1 x =
    6.28   (typ2 -- Scan.repeat const >> (fn (T, cs) => fold (fn c => fn U => Type (c, [U])) cs T)) x
    6.29  and typ2 x =
    6.30 @@ -77,17 +77,17 @@
    6.31  (* terms *)
    6.32  
    6.33  (*
    6.34 -  term  = !!ident :: typ. term
    6.35 +  term  = \<And>ident :: typ. term
    6.36          | term1
    6.37 -  term1 = term2 ==> ... ==> term2
    6.38 +  term1 = term2 \<Longrightarrow> ... \<Longrightarrow> term2
    6.39          | term2
    6.40 -  term2 = term3 == term2
    6.41 +  term2 = term3 \<equiv> term2
    6.42          | term3 &&& term2
    6.43          | term3
    6.44    term3 = ident :: typ
    6.45          | var :: typ
    6.46          | CONST const :: typ
    6.47 -        | %ident :: typ. term3
    6.48 +        | \<lambda>ident :: typ. term3
    6.49          | term4
    6.50    term4 = term5 ... term5
    6.51          | term5
    6.52 @@ -104,23 +104,23 @@
    6.53  val bind = idt --| $$ ".";
    6.54  
    6.55  fun term env T x =
    6.56 - ($$ "!!" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) ||
    6.57 + ($$ "\<And>" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) ||
    6.58    term1 env T) x
    6.59  and term1 env T x =
    6.60 - (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
    6.61 + (enum2 "\<Longrightarrow>" (term2 env propT) >> foldr1 Logic.mk_implies ||
    6.62    term2 env T) x
    6.63  and term2 env T x =
    6.64   (equal env ||
    6.65    term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
    6.66    term3 env T) x
    6.67  and equal env x =
    6.68 - (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) =>
    6.69 + (term3 env dummyT -- ($$ "\<equiv>" |-- term2 env dummyT) >> (fn (t, u) =>
    6.70     Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
    6.71  and term3 env T x =
    6.72   (idt >> Free ||
    6.73    var -- constraint >> Var ||
    6.74    $$ "CONST" |-- const -- constraint >> Const ||
    6.75 -  $$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
    6.76 +  $$ "\<lambda>" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
    6.77    term4 env T) x
    6.78  and term4 env T x =
    6.79   (term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb ||
    6.80 @@ -132,7 +132,10 @@
    6.81    $$ "(" |-- term env T --| $$ ")") x;
    6.82  
    6.83  fun read_tm T s =
    6.84 -  let val t = read (term [] T) s in
    6.85 +  let
    6.86 +    val t = read (term [] T) s
    6.87 +      handle ERROR msg => cat_error ("Malformed input " ^ quote s) msg;
    6.88 +  in
    6.89      if can (Term.map_types Term.no_dummyT) t then t
    6.90      else error ("Unspecified types in input: " ^ quote s)
    6.91    end;
     7.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Feb 25 12:59:08 2018 +0100
     7.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Feb 25 15:44:46 2018 +0100
     7.3 @@ -245,7 +245,7 @@
     7.4    constants that may be subject to beta-reduction after substitution
     7.5    of frees should not be included for LHS set because they could be
     7.6    thrown away by the substituted function.  E.g. for (?F 1 2) do not
     7.7 -  include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
     7.8 +  include 1 or 2, if it were possible for ?F to be (\<lambda>x y. 3).  The
     7.9    largest possible set should always be included on the RHS.*)
    7.10  
    7.11  fun filter_pattern ctxt pat =
     8.1 --- a/src/Pure/assumption.ML	Sun Feb 25 12:59:08 2018 +0100
     8.2 +++ b/src/Pure/assumption.ML	Sun Feb 25 15:44:46 2018 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4       :
     8.5       B
     8.6    --------
     8.7 -  #A ==> B
     8.8 +  #A \<Longrightarrow> B
     8.9  *)
    8.10  fun assume_export is_goal asms =
    8.11    (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
    8.12 @@ -44,7 +44,7 @@
    8.13       :
    8.14       B
    8.15    -------
    8.16 -  A ==> B
    8.17 +  A \<Longrightarrow> B
    8.18  *)
    8.19  fun presume_export _ = assume_export false;
    8.20  
    8.21 @@ -60,7 +60,7 @@
    8.22  (** local context data **)
    8.23  
    8.24  datatype data = Data of
    8.25 - {assms: (export * cterm list) list,    (*assumes: A ==> _*)
    8.26 + {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
    8.27    prems: thm list};                     (*prems: A |- norm_hhf A*)
    8.28  
    8.29  fun make_data (assms, prems) = Data {assms = assms, prems = prems};
     9.1 --- a/src/Pure/conjunction.ML	Sun Feb 25 12:59:08 2018 +0100
     9.2 +++ b/src/Pure/conjunction.ML	Sun Feb 25 15:44:46 2018 +0100
     9.3 @@ -72,7 +72,7 @@
     9.4  val A = read_prop "A" and vA = (("A", 0), propT);
     9.5  val B = read_prop "B" and vB = (("B", 0), propT);
     9.6  val C = read_prop "C";
     9.7 -val ABC = read_prop "A ==> B ==> C";
     9.8 +val ABC = read_prop "A \<Longrightarrow> B \<Longrightarrow> C";
     9.9  val A_B = read_prop "A &&& B";
    9.10  
    9.11  val conjunction_def =
    9.12 @@ -155,9 +155,9 @@
    9.13  in
    9.14  
    9.15  (*
    9.16 -  A1 &&& ... &&& An ==> B
    9.17 +  A1 &&& ... &&& An \<Longrightarrow> B
    9.18    -----------------------
    9.19 -  A1 ==> ... ==> An ==> B
    9.20 +  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B
    9.21  *)
    9.22  fun curry_balanced n th =
    9.23    if n < 2 then th
    9.24 @@ -172,9 +172,9 @@
    9.25      end;
    9.26  
    9.27  (*
    9.28 -  A1 ==> ... ==> An ==> B
    9.29 +  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B
    9.30    -----------------------
    9.31 -  A1 &&& ... &&& An ==> B
    9.32 +  A1 &&& ... &&& An \<Longrightarrow> B
    9.33  *)
    9.34  fun uncurry_balanced n th =
    9.35    if n < 2 then th
    10.1 --- a/src/Pure/conv.ML	Sun Feb 25 12:59:08 2018 +0100
    10.2 +++ b/src/Pure/conv.ML	Sun Feb 25 15:44:46 2018 +0100
    10.3 @@ -176,20 +176,20 @@
    10.4  
    10.5  (* conversions on HHF rules *)
    10.6  
    10.7 -(*rewrite B in !!x1 ... xn. B*)
    10.8 +(*rewrite B in \<And>x1 ... xn. B*)
    10.9  fun params_conv n cv ctxt ct =
   10.10    if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   10.11    then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   10.12    else cv ctxt ct;
   10.13  
   10.14 -(*rewrite the A's in A1 ==> ... ==> An ==> B*)
   10.15 +(*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
   10.16  fun prems_conv 0 _ ct = all_conv ct
   10.17    | prems_conv n cv ct =
   10.18        (case try Thm.dest_implies ct of
   10.19          NONE => all_conv ct
   10.20        | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
   10.21  
   10.22 -(*rewrite B in A1 ==> ... ==> An ==> B*)
   10.23 +(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
   10.24  fun concl_conv 0 cv ct = cv ct
   10.25    | concl_conv n cv ct =
   10.26        (case try Thm.dest_implies ct of
    11.1 --- a/src/Pure/drule.ML	Sun Feb 25 12:59:08 2018 +0100
    11.2 +++ b/src/Pure/drule.ML	Sun Feb 25 15:44:46 2018 +0100
    11.3 @@ -119,13 +119,13 @@
    11.4  
    11.5  (** some cterm->cterm operations: faster than calling cterm_of! **)
    11.6  
    11.7 -(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    11.8 +(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to  [A1,...,An], where B is not an implication *)
    11.9  fun strip_imp_prems ct =
   11.10    let val (cA, cB) = Thm.dest_implies ct
   11.11    in cA :: strip_imp_prems cB end
   11.12    handle TERM _ => [];
   11.13  
   11.14 -(* A1==>...An==>B  goes to B, where B is not an implication *)
   11.15 +(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to B, where B is not an implication *)
   11.16  fun strip_imp_concl ct =
   11.17    (case Thm.term_of ct of
   11.18      Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
   11.19 @@ -139,7 +139,7 @@
   11.20  val implies = certify Logic.implies;
   11.21  fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
   11.22  
   11.23 -(*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
   11.24 +(*cterm version of list_implies: [A1,...,An], B  goes to \<lbrakk>A1;...;An\<rbrakk>\<Longrightarrow>B *)
   11.25  fun list_implies([], B) = B
   11.26    | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
   11.27  
   11.28 @@ -210,10 +210,10 @@
   11.29  (*specialization over a list of cterms*)
   11.30  val forall_elim_list = fold Thm.forall_elim;
   11.31  
   11.32 -(*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
   11.33 +(*maps A1,...,An |- B  to  \<lbrakk>A1;...;An\<rbrakk> \<Longrightarrow> B*)
   11.34  val implies_intr_list = fold_rev Thm.implies_intr;
   11.35  
   11.36 -(*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
   11.37 +(*maps \<lbrakk>A1;...;An\<rbrakk> \<Longrightarrow> B and [A1,...,An]  to  B*)
   11.38  fun implies_elim_list impth ths = fold Thm.elim_implies ths impth;
   11.39  
   11.40  (*Reset Var indexes to zero, renaming to preserve distinctness*)
   11.41 @@ -309,7 +309,7 @@
   11.42    | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
   11.43    | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
   11.44  
   11.45 -(*Resolution: P==>Q, Q==>R gives P==>R*)
   11.46 +(*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*)
   11.47  fun tha RS thb = tha RSN (1,thb);
   11.48  
   11.49  (*For joining lists of rules*)
   11.50 @@ -332,8 +332,8 @@
   11.51    makes proof trees*)
   11.52  fun rls MRS bottom_rl = bottom_rl OF rls;
   11.53  
   11.54 -(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   11.55 -  with no lifting or renaming!  Q may contain ==> or meta-quants
   11.56 +(*compose Q and \<lbrakk>...,Qi,Q(i+1),...\<rbrakk> \<Longrightarrow> R to \<lbrakk>...,Q(i+1),...\<rbrakk> \<Longrightarrow> R
   11.57 +  with no lifting or renaming!  Q may contain \<Longrightarrow> or meta-quantifiers
   11.58    ALWAYS deletes premise i *)
   11.59  fun compose (tha, i, thb) =
   11.60    Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   11.61 @@ -367,14 +367,14 @@
   11.62  
   11.63  val symmetric_thm =
   11.64    let
   11.65 -    val xy = read_prop "x::'a == y::'a";
   11.66 +    val xy = read_prop "x::'a \<equiv> y::'a";
   11.67      val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
   11.68    in store_standard_thm_open (Binding.make ("symmetric", \<^here>)) thm end;
   11.69  
   11.70  val transitive_thm =
   11.71    let
   11.72 -    val xy = read_prop "x::'a == y::'a";
   11.73 -    val yz = read_prop "y::'a == z::'a";
   11.74 +    val xy = read_prop "x::'a \<equiv> y::'a";
   11.75 +    val yz = read_prop "y::'a \<equiv> z::'a";
   11.76      val xythm = Thm.assume xy;
   11.77      val yzthm = Thm.assume yz;
   11.78      val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
   11.79 @@ -387,13 +387,13 @@
   11.80  
   11.81  val equals_cong =
   11.82    store_standard_thm_open (Binding.make ("equals_cong", \<^here>))
   11.83 -    (Thm.reflexive (read_prop "x::'a == y::'a"));
   11.84 +    (Thm.reflexive (read_prop "x::'a \<equiv> y::'a"));
   11.85  
   11.86  val imp_cong =
   11.87    let
   11.88 -    val ABC = read_prop "A ==> B::prop == C::prop"
   11.89 -    val AB = read_prop "A ==> B"
   11.90 -    val AC = read_prop "A ==> C"
   11.91 +    val ABC = read_prop "A \<Longrightarrow> B::prop \<equiv> C::prop"
   11.92 +    val AB = read_prop "A \<Longrightarrow> B"
   11.93 +    val AC = read_prop "A \<Longrightarrow> C"
   11.94      val A = read_prop "A"
   11.95    in
   11.96      store_standard_thm_open (Binding.make ("imp_cong", \<^here>))
   11.97 @@ -408,8 +408,8 @@
   11.98  
   11.99  val swap_prems_eq =
  11.100    let
  11.101 -    val ABC = read_prop "A ==> B ==> C"
  11.102 -    val BAC = read_prop "B ==> A ==> C"
  11.103 +    val ABC = read_prop "A \<Longrightarrow> B \<Longrightarrow> C"
  11.104 +    val BAC = read_prop "B \<Longrightarrow> A \<Longrightarrow> C"
  11.105      val A = read_prop "A"
  11.106      val B = read_prop "B"
  11.107    in
  11.108 @@ -439,9 +439,9 @@
  11.109  (* abs_def *)
  11.110  
  11.111  (*
  11.112 -   f ?x1 ... ?xn == u
  11.113 +   f ?x1 ... ?xn \<equiv> u
  11.114    --------------------
  11.115 -   f == %x1 ... xn. u
  11.116 +   f \<equiv> \<lambda>x1 ... xn. u
  11.117  *)
  11.118  
  11.119  local
  11.120 @@ -476,17 +476,17 @@
  11.121    store_standard_thm_open (Binding.make ("asm_rl", \<^here>))
  11.122      (Thm.trivial (read_prop "?psi"));
  11.123  
  11.124 -(*Meta-level cut rule: [| V==>W; V |] ==> W *)
  11.125 +(*Meta-level cut rule: \<lbrakk>V \<Longrightarrow> W; V\<rbrakk> \<Longrightarrow> W *)
  11.126  val cut_rl =
  11.127    store_standard_thm_open (Binding.make ("cut_rl", \<^here>))
  11.128 -    (Thm.trivial (read_prop "?psi ==> ?theta"));
  11.129 +    (Thm.trivial (read_prop "?psi \<Longrightarrow> ?theta"));
  11.130  
  11.131  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
  11.132 -     [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
  11.133 +     \<lbrakk>PROP V; PROP V \<Longrightarrow> PROP W\<rbrakk> \<Longrightarrow> PROP W *)
  11.134  val revcut_rl =
  11.135    let
  11.136      val V = read_prop "V";
  11.137 -    val VW = read_prop "V ==> W";
  11.138 +    val VW = read_prop "V \<Longrightarrow> W";
  11.139    in
  11.140      store_standard_thm_open (Binding.make ("revcut_rl", \<^here>))
  11.141        (Thm.implies_intr V
  11.142 @@ -501,11 +501,11 @@
  11.143      val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
  11.144    in store_standard_thm_open (Binding.make ("thin_rl", \<^here>)) thm end;
  11.145  
  11.146 -(* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
  11.147 +(* (\<And>x. PROP ?V) \<equiv> PROP ?V       Allows removal of redundant parameters*)
  11.148  val triv_forall_equality =
  11.149    let
  11.150      val V = read_prop "V";
  11.151 -    val QV = read_prop "!!x::'a. V";
  11.152 +    val QV = read_prop "\<And>x::'a. V";
  11.153      val x = certify (Free ("x", Term.aT []));
  11.154    in
  11.155      store_standard_thm_open (Binding.make ("triv_forall_equality", \<^here>))
  11.156 @@ -513,12 +513,12 @@
  11.157          (Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
  11.158    end;
  11.159  
  11.160 -(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==>
  11.161 -   (PROP ?Phi ==> PROP ?Psi)
  11.162 +(* (PROP ?Phi \<Longrightarrow> PROP ?Phi \<Longrightarrow> PROP ?Psi) \<Longrightarrow>
  11.163 +   (PROP ?Phi \<Longrightarrow> PROP ?Psi)
  11.164  *)
  11.165  val distinct_prems_rl =
  11.166    let
  11.167 -    val AAB = read_prop "Phi ==> Phi ==> Psi";
  11.168 +    val AAB = read_prop "Phi \<Longrightarrow> Phi \<Longrightarrow> Psi";
  11.169      val A = read_prop "Phi";
  11.170    in
  11.171      store_standard_thm_open (Binding.make ("distinct_prems_rl", \<^here>))
  11.172 @@ -526,36 +526,36 @@
  11.173          (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
  11.174    end;
  11.175  
  11.176 -(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
  11.177 -   ==> PROP ?phi == PROP ?psi
  11.178 -   Introduction rule for == as a meta-theorem.
  11.179 +(* \<lbrakk>PROP ?phi \<Longrightarrow> PROP ?psi; PROP ?psi \<Longrightarrow> PROP ?phi\<rbrakk>
  11.180 +   \<Longrightarrow> PROP ?phi \<equiv> PROP ?psi
  11.181 +   Introduction rule for \<equiv> as a meta-theorem.
  11.182  *)
  11.183  val equal_intr_rule =
  11.184    let
  11.185 -    val PQ = read_prop "phi ==> psi";
  11.186 -    val QP = read_prop "psi ==> phi";
  11.187 +    val PQ = read_prop "phi \<Longrightarrow> psi";
  11.188 +    val QP = read_prop "psi \<Longrightarrow> phi";
  11.189    in
  11.190      store_standard_thm_open (Binding.make ("equal_intr_rule", \<^here>))
  11.191        (Thm.implies_intr PQ
  11.192          (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
  11.193    end;
  11.194  
  11.195 -(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
  11.196 +(* PROP ?phi \<equiv> PROP ?psi \<Longrightarrow> PROP ?phi \<Longrightarrow> PROP ?psi *)
  11.197  val equal_elim_rule1 =
  11.198    let
  11.199 -    val eq = read_prop "phi::prop == psi::prop";
  11.200 +    val eq = read_prop "phi::prop \<equiv> psi::prop";
  11.201      val P = read_prop "phi";
  11.202    in
  11.203      store_standard_thm_open (Binding.make ("equal_elim_rule1", \<^here>))
  11.204        (Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
  11.205    end;
  11.206  
  11.207 -(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
  11.208 +(* PROP ?psi \<equiv> PROP ?phi \<Longrightarrow> PROP ?phi \<Longrightarrow> PROP ?psi *)
  11.209  val equal_elim_rule2 =
  11.210    store_standard_thm_open (Binding.make ("equal_elim_rule2", \<^here>))
  11.211      (symmetric_thm RS equal_elim_rule1);
  11.212  
  11.213 -(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
  11.214 +(* PROP ?phi \<Longrightarrow> PROP ?phi \<Longrightarrow> PROP ?psi \<Longrightarrow> PROP ?psi *)
  11.215  val remdups_rl =
  11.216    let
  11.217      val P = read_prop "phi";
  11.218 @@ -652,7 +652,7 @@
  11.219  
  11.220  (* HHF normalization *)
  11.221  
  11.222 -(* (PROP ?phi ==> (!!x. PROP ?psi x)) == (!!x. PROP ?phi ==> PROP ?psi x) *)
  11.223 +(* (PROP ?phi \<Longrightarrow> (\<And>x. PROP ?psi x)) \<equiv> (\<And>x. PROP ?phi \<Longrightarrow> PROP ?psi x) *)
  11.224  val norm_hhf_eq =
  11.225    let
  11.226      val aT = TFree ("'a", []);
  11.227 @@ -710,7 +710,7 @@
  11.228  
  11.229  local
  11.230  
  11.231 -(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
  11.232 +(*compose Q and \<lbrakk>Q1,Q2,...,Qk\<rbrakk> \<Longrightarrow> R to \<lbrakk>Q2,...,Qk\<rbrakk> \<Longrightarrow> R getting unique result*)
  11.233  fun comp incremented th1 th2 =
  11.234    Thm.bicompose NONE {flatten = true, match = false, incremented = incremented}
  11.235      (false, th1, 0) 1 th2
    12.1 --- a/src/Pure/goal.ML	Sun Feb 25 12:59:08 2018 +0100
    12.2 +++ b/src/Pure/goal.ML	Sun Feb 25 15:44:46 2018 +0100
    12.3 @@ -60,21 +60,21 @@
    12.4  
    12.5  (*
    12.6    -------- (init)
    12.7 -  C ==> #C
    12.8 +  C \<Longrightarrow> #C
    12.9  *)
   12.10  fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
   12.11  
   12.12  (*
   12.13 -  A1 ==> ... ==> An ==> C
   12.14 +  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C
   12.15    ------------------------ (protect n)
   12.16 -  A1 ==> ... ==> An ==> #C
   12.17 +  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> #C
   12.18  *)
   12.19  fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
   12.20  
   12.21  (*
   12.22 -  A ==> ... ==> #C
   12.23 +  A \<Longrightarrow> ... \<Longrightarrow> #C
   12.24    ---------------- (conclude)
   12.25 -  A ==> ... ==> C
   12.26 +  A \<Longrightarrow> ... \<Longrightarrow> C
   12.27  *)
   12.28  fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
   12.29  
    13.1 --- a/src/Pure/logic.ML	Sun Feb 25 12:59:08 2018 +0100
    13.2 +++ b/src/Pure/logic.ML	Sun Feb 25 15:44:46 2018 +0100
    13.3 @@ -173,19 +173,19 @@
    13.4  
    13.5  (** nested implications **)
    13.6  
    13.7 -(* [A1,...,An], B  goes to  A1==>...An==>B  *)
    13.8 +(* [A1,...,An], B  goes to  A1\<Longrightarrow>...An\<Longrightarrow>B  *)
    13.9  fun list_implies ([], B) = B
   13.10    | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   13.11  
   13.12 -(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   13.13 +(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to  [A1,...,An], where B is not an implication *)
   13.14  fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
   13.15    | strip_imp_prems _ = [];
   13.16  
   13.17 -(* A1==>...An==>B  goes to B, where B is not an implication *)
   13.18 +(* A1\<Longrightarrow>...An\<Longrightarrow>B  goes to B, where B is not an implication *)
   13.19  fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
   13.20    | strip_imp_concl A = A : term;
   13.21  
   13.22 -(*Strip and return premises: (i, [], A1==>...Ai==>B)
   13.23 +(*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B)
   13.24      goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   13.25    if  i<0 or else i too big then raises  TERM*)
   13.26  fun strip_prems (0, As, B) = (As, B)
   13.27 @@ -197,13 +197,13 @@
   13.28  fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
   13.29    | count_prems _ = 0;
   13.30  
   13.31 -(*Select Ai from A1 ==>...Ai==>B*)
   13.32 +(*Select Ai from A1\<Longrightarrow>...Ai\<Longrightarrow>B*)
   13.33  fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
   13.34    | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
   13.35    | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   13.36  
   13.37  (*strip a proof state (Horn clause):
   13.38 -  B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   13.39 +  B1 \<Longrightarrow> ... Bn \<Longrightarrow> C   goes to   ([B1, ..., Bn], C) *)
   13.40  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   13.41  
   13.42  
   13.43 @@ -406,7 +406,7 @@
   13.44  fun combound (t, n, k) =
   13.45      if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   13.46  
   13.47 -(* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   13.48 +(* ([xn,...,x1], t)   goes to   \<lambda>x1 ... xn. t *)
   13.49  fun rlist_abs ([], body) = body
   13.50    | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   13.51  
   13.52 @@ -529,11 +529,11 @@
   13.53     HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   13.54    where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   13.55    the the parameters to be flattened, but it allows erule to work on
   13.56 -  assumptions of the form !!x. phi. Any !! after the outermost string
   13.57 +  assumptions of the form \<And>x. phi. Any \<And> after the outermost string
   13.58    will be regarded as belonging to the conclusion, and left untouched.
   13.59    Used ONLY by assum_pairs.
   13.60        Unless nasms<0, it can terminate the recursion early; that allows
   13.61 -  erule to work on assumptions of the form P==>Q.*)
   13.62 +  erule to work on assumptions of the form P\<Longrightarrow>Q.*)
   13.63  fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   13.64    | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
   13.65        strip_assums_imp (nasms-1, H::Hs, B)
   13.66 @@ -546,9 +546,9 @@
   13.67  
   13.68  (*Produces disagreement pairs, one for each assumption proof, in order.
   13.69    A is the first premise of the lifted rule, and thus has the form
   13.70 -    H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   13.71 +    H1 \<Longrightarrow> ... Hk \<Longrightarrow> B   and the pairs are (H1,B),...,(Hk,B).
   13.72    nasms is the number of assumptions in the original subgoal, needed when B
   13.73 -    has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   13.74 +    has the form B1 \<Longrightarrow> B2: it stops B1 from being taken as an assumption. *)
   13.75  fun assum_pairs(nasms,A) =
   13.76    let val (params, A') = strip_assums_all ([],A)
   13.77        val (Hs,B) = strip_assums_imp (nasms,[],A')
    14.1 --- a/src/Pure/more_thm.ML	Sun Feb 25 12:59:08 2018 +0100
    14.2 +++ b/src/Pure/more_thm.ML	Sun Feb 25 15:44:46 2018 +0100
    14.3 @@ -350,7 +350,7 @@
    14.4  (** basic derived rules **)
    14.5  
    14.6  (*Elimination of implication
    14.7 -  A    A ==> B
    14.8 +  A    A \<Longrightarrow> B
    14.9    ------------
   14.10          B
   14.11  *)
    15.1 --- a/src/Pure/primitive_defs.ML	Sun Feb 25 12:59:08 2018 +0100
    15.2 +++ b/src/Pure/primitive_defs.ML	Sun Feb 25 15:44:46 2018 +0100
    15.3 @@ -23,7 +23,7 @@
    15.4    | term_kind (Bound _) = "bound variable "
    15.5    | term_kind _ = "";
    15.6  
    15.7 -(*c x == t[x] to !!x. c x == t[x]*)
    15.8 +(*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*)
    15.9  fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq =
   15.10    let
   15.11      fun err msg = raise TERM (msg, [eq]);
   15.12 @@ -72,7 +72,7 @@
   15.13          fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
   15.14    end;
   15.15  
   15.16 -(*!!x. c x == t[x] to c == %x. t[x]*)
   15.17 +(*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*)
   15.18  fun abs_def eq =
   15.19    let
   15.20      val body = Term.strip_all_body eq;
    16.1 --- a/src/Pure/pure_thy.ML	Sun Feb 25 12:59:08 2018 +0100
    16.2 +++ b/src/Pure/pure_thy.ML	Sun Feb 25 15:44:46 2018 +0100
    16.3 @@ -31,14 +31,14 @@
    16.4  (* application syntax variants *)
    16.5  
    16.6  val appl_syntax =
    16.7 - [("_appl", typ "('b => 'a) => args => logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
    16.8 -  ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    16.9 + [("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
   16.10 +  ("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
   16.11  
   16.12  val applC_syntax =
   16.13 - [("",       typ "'a => cargs",                  Mixfix.mixfix "_"),
   16.14 -  ("_cargs", typ "'a => cargs => cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
   16.15 -  ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
   16.16 -  ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
   16.17 + [("",       typ "'a \<Rightarrow> cargs",                  Mixfix.mixfix "_"),
   16.18 +  ("_cargs", typ "'a \<Rightarrow> cargs \<Rightarrow> cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
   16.19 +  ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
   16.20 +  ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
   16.21  
   16.22  structure Old_Appl_Syntax = Theory_Data
   16.23  (
   16.24 @@ -86,119 +86,119 @@
   16.25          "class_name"]))
   16.26    #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   16.27    #> Sign.add_syntax Syntax.mode_default
   16.28 -   [("",            typ "prop' => prop",               Mixfix.mixfix "_"),
   16.29 -    ("",            typ "logic => any",                Mixfix.mixfix "_"),
   16.30 -    ("",            typ "prop' => any",                Mixfix.mixfix "_"),
   16.31 -    ("",            typ "logic => logic",              Mixfix.mixfix "'(_')"),
   16.32 -    ("",            typ "prop' => prop'",              Mixfix.mixfix "'(_')"),
   16.33 -    ("_constrain",  typ "logic => type => logic",      mixfix ("_::_", [4, 0], 3)),
   16.34 -    ("_constrain",  typ "prop' => type => prop'",      mixfix ("_::_", [4, 0], 3)),
   16.35 +   [("",            typ "prop' \<Rightarrow> prop",               Mixfix.mixfix "_"),
   16.36 +    ("",            typ "logic \<Rightarrow> any",                Mixfix.mixfix "_"),
   16.37 +    ("",            typ "prop' \<Rightarrow> any",                Mixfix.mixfix "_"),
   16.38 +    ("",            typ "logic \<Rightarrow> logic",              Mixfix.mixfix "'(_')"),
   16.39 +    ("",            typ "prop' \<Rightarrow> prop'",              Mixfix.mixfix "'(_')"),
   16.40 +    ("_constrain",  typ "logic \<Rightarrow> type \<Rightarrow> logic",      mixfix ("_::_", [4, 0], 3)),
   16.41 +    ("_constrain",  typ "prop' \<Rightarrow> type \<Rightarrow> prop'",      mixfix ("_::_", [4, 0], 3)),
   16.42      ("_ignore_type", typ "'a",                         NoSyn),
   16.43 -    ("",            typ "tid_position => type",        Mixfix.mixfix "_"),
   16.44 -    ("",            typ "tvar_position => type",       Mixfix.mixfix "_"),
   16.45 -    ("",            typ "type_name => type",           Mixfix.mixfix "_"),
   16.46 -    ("_type_name",  typ "id => type_name",             Mixfix.mixfix "_"),
   16.47 -    ("_type_name",  typ "longid => type_name",         Mixfix.mixfix "_"),
   16.48 -    ("_ofsort",     typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
   16.49 -    ("_ofsort",     typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
   16.50 -    ("_dummy_ofsort", typ "sort => type",              mixfix ("'_()::_", [0], 1000)),
   16.51 -    ("",            typ "class_name => sort",          Mixfix.mixfix "_"),
   16.52 -    ("_class_name", typ "id => class_name",            Mixfix.mixfix "_"),
   16.53 -    ("_class_name", typ "longid => class_name",        Mixfix.mixfix "_"),
   16.54 +    ("",            typ "tid_position \<Rightarrow> type",        Mixfix.mixfix "_"),
   16.55 +    ("",            typ "tvar_position \<Rightarrow> type",       Mixfix.mixfix "_"),
   16.56 +    ("",            typ "type_name \<Rightarrow> type",           Mixfix.mixfix "_"),
   16.57 +    ("_type_name",  typ "id \<Rightarrow> type_name",             Mixfix.mixfix "_"),
   16.58 +    ("_type_name",  typ "longid \<Rightarrow> type_name",         Mixfix.mixfix "_"),
   16.59 +    ("_ofsort",     typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
   16.60 +    ("_ofsort",     typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
   16.61 +    ("_dummy_ofsort", typ "sort \<Rightarrow> type",              mixfix ("'_()::_", [0], 1000)),
   16.62 +    ("",            typ "class_name \<Rightarrow> sort",          Mixfix.mixfix "_"),
   16.63 +    ("_class_name", typ "id \<Rightarrow> class_name",            Mixfix.mixfix "_"),
   16.64 +    ("_class_name", typ "longid \<Rightarrow> class_name",        Mixfix.mixfix "_"),
   16.65      ("_dummy_sort", typ "sort",                        Mixfix.mixfix "'_"),
   16.66      ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
   16.67 -    ("_sort",       typ "classes => sort",             Mixfix.mixfix "{_}"),
   16.68 -    ("",            typ "class_name => classes",       Mixfix.mixfix "_"),
   16.69 -    ("_classes",    typ "class_name => classes => classes", Mixfix.mixfix "_,_"),
   16.70 -    ("_tapp",       typ "type => type_name => type",   mixfix ("_ _", [1000, 0], 1000)),
   16.71 -    ("_tappl",      typ "type => types => type_name => type", Mixfix.mixfix "((1'(_,/ _')) _)"),
   16.72 -    ("",            typ "type => types",               Mixfix.mixfix "_"),
   16.73 -    ("_types",      typ "type => types => types",      Mixfix.mixfix "_,/ _"),
   16.74 -    ("\<^type>fun", typ "type => type => type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
   16.75 -    ("_bracket",    typ "types => type => type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
   16.76 -    ("",            typ "type => type",                Mixfix.mixfix "'(_')"),
   16.77 +    ("_sort",       typ "classes \<Rightarrow> sort",             Mixfix.mixfix "{_}"),
   16.78 +    ("",            typ "class_name \<Rightarrow> classes",       Mixfix.mixfix "_"),
   16.79 +    ("_classes",    typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"),
   16.80 +    ("_tapp",       typ "type \<Rightarrow> type_name \<Rightarrow> type",   mixfix ("_ _", [1000, 0], 1000)),
   16.81 +    ("_tappl",      typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type", Mixfix.mixfix "((1'(_,/ _')) _)"),
   16.82 +    ("",            typ "type \<Rightarrow> types",               Mixfix.mixfix "_"),
   16.83 +    ("_types",      typ "type \<Rightarrow> types \<Rightarrow> types",      Mixfix.mixfix "_,/ _"),
   16.84 +    ("\<^type>fun", typ "type \<Rightarrow> type \<Rightarrow> type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
   16.85 +    ("_bracket",    typ "types \<Rightarrow> type \<Rightarrow> type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
   16.86 +    ("",            typ "type \<Rightarrow> type",                Mixfix.mixfix "'(_')"),
   16.87      ("\<^type>dummy", typ "type",                      Mixfix.mixfix "'_"),
   16.88      ("_type_prop",  typ "'a",                          NoSyn),
   16.89 -    ("_lambda",     typ "pttrns => 'a => logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
   16.90 +    ("_lambda",     typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
   16.91      ("_abs",        typ "'a",                          NoSyn),
   16.92 -    ("",            typ "'a => args",                  Mixfix.mixfix "_"),
   16.93 -    ("_args",       typ "'a => args => args",          Mixfix.mixfix "_,/ _"),
   16.94 -    ("",            typ "id_position => idt",          Mixfix.mixfix "_"),
   16.95 +    ("",            typ "'a \<Rightarrow> args",                  Mixfix.mixfix "_"),
   16.96 +    ("_args",       typ "'a \<Rightarrow> args \<Rightarrow> args",          Mixfix.mixfix "_,/ _"),
   16.97 +    ("",            typ "id_position \<Rightarrow> idt",          Mixfix.mixfix "_"),
   16.98      ("_idtdummy",   typ "idt",                         Mixfix.mixfix "'_"),
   16.99 -    ("_idtyp",      typ "id_position => type => idt",  mixfix ("_::_", [], 0)),
  16.100 -    ("_idtypdummy", typ "type => idt",                 mixfix ("'_()::_", [], 0)),
  16.101 -    ("",            typ "idt => idt",                  Mixfix.mixfix "'(_')"),
  16.102 -    ("",            typ "idt => idts",                 Mixfix.mixfix "_"),
  16.103 -    ("_idts",       typ "idt => idts => idts",         mixfix ("_/ _", [1, 0], 0)),
  16.104 -    ("",            typ "idt => pttrn",                Mixfix.mixfix "_"),
  16.105 -    ("",            typ "pttrn => pttrns",             Mixfix.mixfix "_"),
  16.106 -    ("_pttrns",     typ "pttrn => pttrns => pttrns",   mixfix ("_/ _", [1, 0], 0)),
  16.107 -    ("",            typ "aprop => aprop",              Mixfix.mixfix "'(_')"),
  16.108 -    ("",            typ "id_position => aprop",        Mixfix.mixfix "_"),
  16.109 -    ("",            typ "longid_position => aprop",    Mixfix.mixfix "_"),
  16.110 -    ("",            typ "var_position => aprop",       Mixfix.mixfix "_"),
  16.111 +    ("_idtyp",      typ "id_position \<Rightarrow> type \<Rightarrow> idt",  mixfix ("_::_", [], 0)),
  16.112 +    ("_idtypdummy", typ "type \<Rightarrow> idt",                 mixfix ("'_()::_", [], 0)),
  16.113 +    ("",            typ "idt \<Rightarrow> idt",                  Mixfix.mixfix "'(_')"),
  16.114 +    ("",            typ "idt \<Rightarrow> idts",                 Mixfix.mixfix "_"),
  16.115 +    ("_idts",       typ "idt \<Rightarrow> idts \<Rightarrow> idts",         mixfix ("_/ _", [1, 0], 0)),
  16.116 +    ("",            typ "idt \<Rightarrow> pttrn",                Mixfix.mixfix "_"),
  16.117 +    ("",            typ "pttrn \<Rightarrow> pttrns",             Mixfix.mixfix "_"),
  16.118 +    ("_pttrns",     typ "pttrn \<Rightarrow> pttrns \<Rightarrow> pttrns",   mixfix ("_/ _", [1, 0], 0)),
  16.119 +    ("",            typ "aprop \<Rightarrow> aprop",              Mixfix.mixfix "'(_')"),
  16.120 +    ("",            typ "id_position \<Rightarrow> aprop",        Mixfix.mixfix "_"),
  16.121 +    ("",            typ "longid_position \<Rightarrow> aprop",    Mixfix.mixfix "_"),
  16.122 +    ("",            typ "var_position \<Rightarrow> aprop",       Mixfix.mixfix "_"),
  16.123      ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
  16.124 -    ("_aprop",      typ "aprop => prop",               Mixfix.mixfix "PROP _"),
  16.125 -    ("_asm",        typ "prop => asms",                Mixfix.mixfix "_"),
  16.126 -    ("_asms",       typ "prop => asms => asms",        Mixfix.mixfix "_;/ _"),
  16.127 -    ("_bigimpl",    typ "asms => prop => prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
  16.128 -    ("_ofclass",    typ "type => logic => prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
  16.129 +    ("_aprop",      typ "aprop \<Rightarrow> prop",               Mixfix.mixfix "PROP _"),
  16.130 +    ("_asm",        typ "prop \<Rightarrow> asms",                Mixfix.mixfix "_"),
  16.131 +    ("_asms",       typ "prop \<Rightarrow> asms \<Rightarrow> asms",        Mixfix.mixfix "_;/ _"),
  16.132 +    ("_bigimpl",    typ "asms \<Rightarrow> prop \<Rightarrow> prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
  16.133 +    ("_ofclass",    typ "type \<Rightarrow> logic \<Rightarrow> prop",       Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"),
  16.134      ("_mk_ofclass", typ "dummy",                       NoSyn),
  16.135 -    ("_TYPE",       typ "type => logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
  16.136 -    ("",            typ "id_position => logic",        Mixfix.mixfix "_"),
  16.137 -    ("",            typ "longid_position => logic",    Mixfix.mixfix "_"),
  16.138 -    ("",            typ "var_position => logic",       Mixfix.mixfix "_"),
  16.139 +    ("_TYPE",       typ "type \<Rightarrow> logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
  16.140 +    ("",            typ "id_position \<Rightarrow> logic",        Mixfix.mixfix "_"),
  16.141 +    ("",            typ "longid_position \<Rightarrow> logic",    Mixfix.mixfix "_"),
  16.142 +    ("",            typ "var_position \<Rightarrow> logic",       Mixfix.mixfix "_"),
  16.143      ("_DDDOT",      typ "logic",                       Mixfix.mixfix "\<dots>"),
  16.144      ("_strip_positions", typ "'a", NoSyn),
  16.145 -    ("_position",   typ "num_token => num_position",   Mixfix.mixfix "_"),
  16.146 -    ("_position",   typ "float_token => float_position", Mixfix.mixfix "_"),
  16.147 -    ("_constify",   typ "num_position => num_const",   Mixfix.mixfix "_"),
  16.148 -    ("_constify",   typ "float_position => float_const", Mixfix.mixfix "_"),
  16.149 -    ("_index",      typ "logic => index",              Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
  16.150 +    ("_position",   typ "num_token \<Rightarrow> num_position",   Mixfix.mixfix "_"),
  16.151 +    ("_position",   typ "float_token \<Rightarrow> float_position", Mixfix.mixfix "_"),
  16.152 +    ("_constify",   typ "num_position \<Rightarrow> num_const",   Mixfix.mixfix "_"),
  16.153 +    ("_constify",   typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"),
  16.154 +    ("_index",      typ "logic \<Rightarrow> index",              Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
  16.155      ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
  16.156      ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
  16.157 -    ("_struct",     typ "index => logic",              NoSyn),
  16.158 +    ("_struct",     typ "index \<Rightarrow> logic",              NoSyn),
  16.159      ("_update_name", typ "idt",                        NoSyn),
  16.160      ("_constrainAbs", typ "'a",                        NoSyn),
  16.161 -    ("_position_sort", typ "tid => tid_position",      Mixfix.mixfix "_"),
  16.162 -    ("_position_sort", typ "tvar => tvar_position",    Mixfix.mixfix "_"),
  16.163 -    ("_position",   typ "id => id_position",           Mixfix.mixfix "_"),
  16.164 -    ("_position",   typ "longid => longid_position",   Mixfix.mixfix "_"),
  16.165 -    ("_position",   typ "var => var_position",         Mixfix.mixfix "_"),
  16.166 -    ("_position",   typ "str_token => str_position",   Mixfix.mixfix "_"),
  16.167 -    ("_position",   typ "string_token => string_position", Mixfix.mixfix "_"),
  16.168 -    ("_position",   typ "cartouche => cartouche_position", Mixfix.mixfix "_"),
  16.169 +    ("_position_sort", typ "tid \<Rightarrow> tid_position",      Mixfix.mixfix "_"),
  16.170 +    ("_position_sort", typ "tvar \<Rightarrow> tvar_position",    Mixfix.mixfix "_"),
  16.171 +    ("_position",   typ "id \<Rightarrow> id_position",           Mixfix.mixfix "_"),
  16.172 +    ("_position",   typ "longid \<Rightarrow> longid_position",   Mixfix.mixfix "_"),
  16.173 +    ("_position",   typ "var \<Rightarrow> var_position",         Mixfix.mixfix "_"),
  16.174 +    ("_position",   typ "str_token \<Rightarrow> str_position",   Mixfix.mixfix "_"),
  16.175 +    ("_position",   typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"),
  16.176 +    ("_position",   typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"),
  16.177      ("_type_constraint_", typ "'a",                    NoSyn),
  16.178 -    ("_context_const", typ "id_position => logic",     Mixfix.mixfix "CONST _"),
  16.179 -    ("_context_const", typ "id_position => aprop",     Mixfix.mixfix "CONST _"),
  16.180 -    ("_context_const", typ "longid_position => logic", Mixfix.mixfix "CONST _"),
  16.181 -    ("_context_const", typ "longid_position => aprop", Mixfix.mixfix "CONST _"),
  16.182 -    ("_context_xconst", typ "id_position => logic",    Mixfix.mixfix "XCONST _"),
  16.183 -    ("_context_xconst", typ "id_position => aprop",    Mixfix.mixfix "XCONST _"),
  16.184 -    ("_context_xconst", typ "longid_position => logic", Mixfix.mixfix "XCONST _"),
  16.185 -    ("_context_xconst", typ "longid_position => aprop", Mixfix.mixfix "XCONST _"),
  16.186 +    ("_context_const", typ "id_position \<Rightarrow> logic",     Mixfix.mixfix "CONST _"),
  16.187 +    ("_context_const", typ "id_position \<Rightarrow> aprop",     Mixfix.mixfix "CONST _"),
  16.188 +    ("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"),
  16.189 +    ("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"),
  16.190 +    ("_context_xconst", typ "id_position \<Rightarrow> logic",    Mixfix.mixfix "XCONST _"),
  16.191 +    ("_context_xconst", typ "id_position \<Rightarrow> aprop",    Mixfix.mixfix "XCONST _"),
  16.192 +    ("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"),
  16.193 +    ("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"),
  16.194      (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
  16.195 -    ("_sort_constraint", typ "type => prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
  16.196 -    (const "Pure.term", typ "logic => prop",           Mixfix.mixfix "TERM _"),
  16.197 -    (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))]
  16.198 +    ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
  16.199 +    (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
  16.200 +    (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
  16.201    #> Sign.add_syntax Syntax.mode_default applC_syntax
  16.202    #> Sign.add_syntax (Print_Mode.ASCII, true)
  16.203 -   [(tycon "fun",         typ "type => type => type",   mixfix ("(_/ => _)", [1, 0], 0)),
  16.204 -    ("_bracket",          typ "types => type => type",  mixfix ("([_]/ => _)", [0, 0], 0)),
  16.205 -    ("_lambda",           typ "pttrns => 'a => logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
  16.206 -    (const "Pure.eq",     typ "'a => 'a => prop",       infix_ ("==", 2)),
  16.207 -    (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
  16.208 -    (const "Pure.imp",    typ "prop => prop => prop",   infixr_ ("==>", 1)),
  16.209 +   [(tycon "fun",         typ "type \<Rightarrow> type \<Rightarrow> type",   mixfix ("(_/ => _)", [1, 0], 0)),
  16.210 +    ("_bracket",          typ "types \<Rightarrow> type \<Rightarrow> type",  mixfix ("([_]/ => _)", [0, 0], 0)),
  16.211 +    ("_lambda",           typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
  16.212 +    (const "Pure.eq",     typ "'a \<Rightarrow> 'a \<Rightarrow> prop",       infix_ ("==", 2)),
  16.213 +    (const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
  16.214 +    (const "Pure.imp",    typ "prop \<Rightarrow> prop \<Rightarrow> prop",   infixr_ ("==>", 1)),
  16.215      ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
  16.216 -    ("_bigimpl",          typ "asms => prop => prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
  16.217 +    ("_bigimpl",          typ "asms \<Rightarrow> prop \<Rightarrow> prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
  16.218      ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
  16.219    #> Sign.add_syntax ("", false)
  16.220 -   [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
  16.221 +   [(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
  16.222    #> Sign.add_consts
  16.223 -   [(qualify (Binding.make ("eq", \<^here>)), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
  16.224 -    (qualify (Binding.make ("imp", \<^here>)), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
  16.225 -    (qualify (Binding.make ("all", \<^here>)), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
  16.226 -    (qualify (Binding.make ("prop", \<^here>)), typ "prop => prop", NoSyn),
  16.227 +   [(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),
  16.228 +    (qualify (Binding.make ("imp", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("\<Longrightarrow>", 1)),
  16.229 +    (qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)),
  16.230 +    (qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn),
  16.231      (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn),
  16.232      (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_")]
  16.233    #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
  16.234 @@ -210,20 +210,20 @@
  16.235    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
  16.236    #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
  16.237    #> Sign.add_consts
  16.238 -   [(qualify (Binding.make ("term", \<^here>)), typ "'a => prop", NoSyn),
  16.239 -    (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself => prop", NoSyn),
  16.240 -    (qualify (Binding.make ("conjunction", \<^here>)), typ "prop => prop => prop", NoSyn)]
  16.241 +   [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn),
  16.242 +    (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),
  16.243 +    (qualify (Binding.make ("conjunction", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", NoSyn)]
  16.244    #> Sign.local_path
  16.245    #> (Global_Theory.add_defs false o map Thm.no_attributes)
  16.246     [(Binding.make ("prop_def", \<^here>),
  16.247 -      prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
  16.248 +      prop "(CONST Pure.prop :: prop \<Rightarrow> prop) (A::prop) \<equiv> A::prop"),
  16.249      (Binding.make ("term_def", \<^here>),
  16.250 -      prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
  16.251 +      prop "(CONST Pure.term :: 'a \<Rightarrow> prop) (x::'a) \<equiv> (\<And>A::prop. A \<Longrightarrow> A)"),
  16.252      (Binding.make ("sort_constraint_def", \<^here>),
  16.253 -      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
  16.254 -      \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
  16.255 +      prop "(CONST Pure.sort_constraint :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself) \<equiv>\
  16.256 +      \ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"),
  16.257      (Binding.make ("conjunction_def", \<^here>),
  16.258 -      prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
  16.259 +      prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd
  16.260    #> fold (fn (a, prop) =>
  16.261        snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms);
  16.262  
    17.1 --- a/src/Pure/raw_simplifier.ML	Sun Feb 25 12:59:08 2018 +0100
    17.2 +++ b/src/Pure/raw_simplifier.ML	Sun Feb 25 15:44:46 2018 +0100
    17.3 @@ -208,7 +208,7 @@
    17.4    null prems andalso Pattern.matches (Proof_Context.theory_of ctxt) (lhs, rhs)
    17.5      (*the condition "null prems" is necessary because conditional rewrites
    17.6        with extra variables in the conditions may terminate although
    17.7 -      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
    17.8 +      the rhs is an instance of the lhs; example: ?m < ?n \<Longrightarrow> f ?n \<equiv> f ?m *)
    17.9      orelse
   17.10    is_Const lhs andalso not (is_Const rhs);
   17.11  
   17.12 @@ -254,8 +254,8 @@
   17.13      mk_rews:
   17.14        mk: turn simplification thms into rewrite rules;
   17.15        mk_cong: prepare congruence rules;
   17.16 -      mk_sym: turn == around;
   17.17 -      mk_eq_True: turn P into P == True;
   17.18 +      mk_sym: turn \<equiv> around;
   17.19 +      mk_eq_True: turn P into P \<equiv> True;
   17.20      term_ord: for ordered rewriting;*)
   17.21  
   17.22  datatype simpset =
   17.23 @@ -1146,7 +1146,7 @@
   17.24                            NONE => appc ()
   17.25                          | SOME cong =>
   17.26       (*post processing: some partial applications h t1 ... tj, j <= length ts,
   17.27 -       may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
   17.28 +       may be a redex. Example: map (\<lambda>x. x) = (\<lambda>xs. xs) wrt map_cong*)
   17.29                             (let
   17.30                                val thm = congc (prover ctxt) ctxt maxidx cong t0;
   17.31                                val t = the_default t0 (Option.map Thm.rhs_of thm);
   17.32 @@ -1290,14 +1290,14 @@
   17.33    in try_botc end;
   17.34  
   17.35  
   17.36 -(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
   17.37 +(* Meta-rewriting: rewrites t to u and returns the theorem t \<equiv> u *)
   17.38  
   17.39  (*
   17.40    Parameters:
   17.41      mode = (simplify A,
   17.42              use A in simplifying B,
   17.43              use prems of B (if B is again a meta-impl.) to simplify A)
   17.44 -           when simplifying A ==> B
   17.45 +           when simplifying A \<Longrightarrow> B
   17.46      prover: how to solve premises in conditional rewrites and congruences
   17.47  *)
   17.48  
   17.49 @@ -1369,7 +1369,7 @@
   17.50  
   17.51  val lhs_of_thm = #1 o Logic.dest_equals o Thm.prop_of;
   17.52  
   17.53 -(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   17.54 +(*folding should handle critical pairs!  E.g. K \<equiv> Inl 0,  S \<equiv> Inr (Inl 0)
   17.55    Returns longest lhs first to avoid folding its subexpressions.*)
   17.56  fun sort_lhs_depths defs =
   17.57    let val keylist = AList.make (term_depth o lhs_of_thm) defs
   17.58 @@ -1382,7 +1382,7 @@
   17.59  fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
   17.60  
   17.61  
   17.62 -(* HHF normal form: !! before ==>, outermost !! generalized *)
   17.63 +(* HHF normal form: \<And> before \<Longrightarrow>, outermost \<And> generalized *)
   17.64  
   17.65  local
   17.66  
    18.1 --- a/src/Pure/tactic.ML	Sun Feb 25 12:59:08 2018 +0100
    18.2 +++ b/src/Pure/tactic.ML	Sun Feb 25 15:44:46 2018 +0100
    18.3 @@ -107,8 +107,8 @@
    18.4  fun compose_tac ctxt arg i =
    18.5    PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i);
    18.6  
    18.7 -(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
    18.8 -  like [| P&Q; P==>R |] ==> R *)
    18.9 +(*Converts a "destruct" rule like P \<and> Q \<Longrightarrow> P to an "elimination" rule
   18.10 +  like \<lbrakk>P \<and> Q; P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R *)
   18.11  fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   18.12  
   18.13  (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
    19.1 --- a/src/Pure/term.ML	Sun Feb 25 12:59:08 2018 +0100
    19.2 +++ b/src/Pure/term.ML	Sun Feb 25 15:44:46 2018 +0100
    19.3 @@ -598,11 +598,11 @@
    19.4  
    19.5  val propT : typ = Type ("prop",[]);
    19.6  
    19.7 -(*maps  !!x1...xn. t   to   t*)
    19.8 +(*maps  \<And>x1...xn. t   to   t*)
    19.9  fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
   19.10    | strip_all_body t = t;
   19.11  
   19.12 -(*maps  !!x1...xn. t   to   [x1, ..., xn]*)
   19.13 +(*maps  \<And>x1...xn. t   to   [x1, ..., xn]*)
   19.14  fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
   19.15    | strip_all_vars t = [];
   19.16  
   19.17 @@ -672,7 +672,7 @@
   19.18  
   19.19  (*Substitute arguments for loose bound variables.
   19.20    Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   19.21 -  Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   19.22 +  Note that for ((\<lambda>x y. c) a b), the bound vars in c are x=1 and y=0
   19.23          and the appropriate call is  subst_bounds([b,a], c) .
   19.24    Loose bound variables >=n are reduced by "n" to
   19.25       compensate for the disappearance of lambdas.
    20.1 --- a/src/Pure/thm.ML	Sun Feb 25 12:59:08 2018 +0100
    20.2 +++ b/src/Pure/thm.ML	Sun Feb 25 15:44:46 2018 +0100
    20.3 @@ -769,7 +769,7 @@
    20.4       :
    20.5       B
    20.6    -------
    20.7 -  A ==> B
    20.8 +  A \<Longrightarrow> B
    20.9  *)
   20.10  fun implies_intr
   20.11      (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})
   20.12 @@ -788,7 +788,7 @@
   20.13  
   20.14  
   20.15  (*Implication elimination
   20.16 -  A ==> B    A
   20.17 +  A \<Longrightarrow> B    A
   20.18    ------------
   20.19          B
   20.20  *)
   20.21 @@ -819,7 +819,7 @@
   20.22       :
   20.23       A
   20.24    ------
   20.25 -  !!x. A
   20.26 +  \<And>x. A
   20.27  *)
   20.28  fun forall_intr
   20.29      (ct as Cterm {t = x, T, sorts, ...})
   20.30 @@ -846,7 +846,7 @@
   20.31    end;
   20.32  
   20.33  (*Forall elimination
   20.34 -  !!x. A
   20.35 +  \<And>x. A
   20.36    ------
   20.37    A[t/x]
   20.38  *)
   20.39 @@ -872,7 +872,7 @@
   20.40  (* Equality *)
   20.41  
   20.42  (*Reflexivity
   20.43 -  t == t
   20.44 +  t \<equiv> t
   20.45  *)
   20.46  fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
   20.47    Thm (deriv_rule0 Proofterm.reflexive,
   20.48 @@ -885,9 +885,9 @@
   20.49      prop = Logic.mk_equals (t, t)});
   20.50  
   20.51  (*Symmetry
   20.52 -  t == u
   20.53 +  t \<equiv> u
   20.54    ------
   20.55 -  u == t
   20.56 +  u \<equiv> t
   20.57  *)
   20.58  fun symmetric (th as Thm (der, {cert, maxidx, shyps, hyps, tpairs, prop, ...})) =
   20.59    (case prop of
   20.60 @@ -903,9 +903,9 @@
   20.61      | _ => raise THM ("symmetric", 0, [th]));
   20.62  
   20.63  (*Transitivity
   20.64 -  t1 == u    u == t2
   20.65 +  t1 \<equiv> u    u \<equiv> t2
   20.66    ------------------
   20.67 -       t1 == t2
   20.68 +       t1 \<equiv> t2
   20.69  *)
   20.70  fun transitive th1 th2 =
   20.71    let
   20.72 @@ -931,7 +931,7 @@
   20.73    end;
   20.74  
   20.75  (*Beta-conversion
   20.76 -  (%x. t)(u) == t[u/x]
   20.77 +  (\<lambda>x. t) u \<equiv> t[u/x]
   20.78    fully beta-reduces the term if full = true
   20.79  *)
   20.80  fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) =
   20.81 @@ -973,9 +973,9 @@
   20.82  
   20.83  (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   20.84    The bound variable will be named "a" (since x will be something like x320)
   20.85 -      t == u
   20.86 +      t \<equiv> u
   20.87    --------------
   20.88 -  %x. t == %x. u
   20.89 +  \<lambda>x. t \<equiv> \<lambda>x. u
   20.90  *)
   20.91  fun abstract_rule a
   20.92      (Cterm {t = x, T, sorts, ...})
   20.93 @@ -1005,9 +1005,9 @@
   20.94    end;
   20.95  
   20.96  (*The combination rule
   20.97 -  f == g  t == u
   20.98 -  --------------
   20.99 -    f t == g u
  20.100 +  f \<equiv> g  t \<equiv> u
  20.101 +  -------------
  20.102 +    f t \<equiv> g u
  20.103  *)
  20.104  fun combination th1 th2 =
  20.105    let
  20.106 @@ -1039,9 +1039,9 @@
  20.107    end;
  20.108  
  20.109  (*Equality introduction
  20.110 -  A ==> B  B ==> A
  20.111 +  A \<Longrightarrow> B  B \<Longrightarrow> A
  20.112    ----------------
  20.113 -       A == B
  20.114 +       A \<equiv> B
  20.115  *)
  20.116  fun equal_intr th1 th2 =
  20.117    let
  20.118 @@ -1067,7 +1067,7 @@
  20.119    end;
  20.120  
  20.121  (*The equal propositions rule
  20.122 -  A == B  A
  20.123 +  A \<equiv> B  A
  20.124    ---------
  20.125        B
  20.126  *)
  20.127 @@ -1110,7 +1110,7 @@
  20.128          else
  20.129            let
  20.130              val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
  20.131 -              (*remove trivial tpairs, of the form t==t*)
  20.132 +              (*remove trivial tpairs, of the form t \<equiv> t*)
  20.133                |> filter_out (op aconv);
  20.134              val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
  20.135              val prop' = Envir.norm_term env prop;
  20.136 @@ -1269,7 +1269,7 @@
  20.137  end;
  20.138  
  20.139  
  20.140 -(*The trivial implication A ==> A, justified by assume and forall rules.
  20.141 +(*The trivial implication A \<Longrightarrow> A, justified by assume and forall rules.
  20.142    A can contain Vars, not so for assume!*)
  20.143  fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) =
  20.144    if T <> propT then
  20.145 @@ -1673,7 +1673,7 @@
  20.146       and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
  20.147       val (context, cert) =
  20.148         make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule));
  20.149 -     (*Add new theorem with prop = '[| Bs; As |] ==> C' to thq*)
  20.150 +     (*Add new theorem with prop = "\<lbrakk>Bs; As\<rbrakk> \<Longrightarrow> C" to thq*)
  20.151       fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
  20.152         let val normt = Envir.norm_term env;
  20.153             (*perform minimal copying here by examining env*)
    21.1 --- a/src/Pure/unify.ML	Sun Feb 25 12:59:08 2018 +0100
    21.2 +++ b/src/Pure/unify.ML	Sun Feb 25 15:44:46 2018 +0100
    21.3 @@ -426,7 +426,7 @@
    21.4  
    21.5  (*If an argument contains a banned Bound, then it should be deleted.
    21.6    But if the only path is flexible, this is difficult; the code gives up!
    21.7 -  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
    21.8 +  In \<lambda>x y. ?a x =?= \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
    21.9  exception CHANGE_FAIL;   (*flexible occurrence of banned variable, or other reason to quit*)
   21.10  
   21.11  
   21.12 @@ -570,7 +570,7 @@
   21.13  
   21.14  
   21.15  (*Print a tracing message + list of dpairs.
   21.16 -  In t==u print u first because it may be rigid or flexible --
   21.17 +  In t \<equiv> u print u first because it may be rigid or flexible --
   21.18      t is always flexible.*)
   21.19  fun print_dpairs context msg (env, dpairs) =
   21.20    if Context_Position.is_visible_generic context then
   21.21 @@ -636,12 +636,12 @@
   21.22  
   21.23  
   21.24  (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   21.25 -  Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   21.26 -  Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
   21.27 +  Unifies ?f t1 ... rm with ?g u1 ... un by ?f -> \<lambda>x1...xm. ?a, ?g -> \<lambda>x1...xn. ?a
   21.28 +  Unfortunately, unifies ?f t u with ?g t u by ?f, ?g -> \<lambda>x y. ?a,
   21.29    though just ?g->?f is a more general unifier.
   21.30    Unlike Huet (1975), does not smash together all variables of same type --
   21.31      requires more work yet gives a less general unifier (fewer variables).
   21.32 -  Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   21.33 +  Handles ?f t1 ... rm with ?f u1 ... um to avoid multiple updates. *)
   21.34  fun smash_flexflex1 (t, u) env : Envir.env =
   21.35    let
   21.36      val vT as (v, T) = var_head_of (env, t)
    22.1 --- a/src/Pure/variable.ML	Sun Feb 25 12:59:08 2018 +0100
    22.2 +++ b/src/Pure/variable.ML	Sun Feb 25 15:44:46 2018 +0100
    22.3 @@ -642,7 +642,7 @@
    22.4  val trade = gen_trade (import true) export;
    22.5  
    22.6  
    22.7 -(* focus on outermost parameters: !!x y z. B *)
    22.8 +(* focus on outermost parameters: \<And>x y z. B *)
    22.9  
   22.10  val bound_focus =
   22.11    Config.bool (Config.declare ("bound_focus", \<^here>) (K (Config.Bool false)));