tuned messages -- more symbols;
authorwenzelm
Sun Dec 18 13:07:13 2016 +0100 (2016-12-18)
changeset 6459651f8e259de50
parent 64595 511b30aa4100
child 64597 1c252d8b6ca6
tuned messages -- more symbols;
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_display.ML
src/Pure/primitive_defs.ML
     1.1 --- a/src/Pure/Isar/overloading.ML	Sun Dec 18 12:34:31 2016 +0100
     1.2 +++ b/src/Pure/Isar/overloading.ML	Sun Dec 18 13:07:13 2016 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4        | NONE => NONE);
     1.5      val unchecks =
     1.6        map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
     1.7 -  in 
     1.8 +  in
     1.9      ctxt
    1.10      |> map_improvable_syntax (K {primary_constraints = [],
    1.11        secondary_constraints = [], improve = K NONE, subst = subst,
    1.12 @@ -168,7 +168,7 @@
    1.13      val overloading = get_overloading lthy;
    1.14      fun pr_operation ((c, ty), (v, _)) =
    1.15        Pretty.block (Pretty.breaks
    1.16 -        [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
    1.17 +        [Pretty.str v, Pretty.str "\<equiv>", Proof_Context.pretty_const lthy c,
    1.18            Pretty.str "::", Syntax.pretty_typ lthy ty]);
    1.19    in
    1.20      [Pretty.block
     2.1 --- a/src/Pure/Isar/proof_display.ML	Sun Dec 18 12:34:31 2016 +0100
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Sun Dec 18 13:07:13 2016 +0100
     2.3 @@ -95,7 +95,7 @@
     2.4      val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
     2.5  
     2.6      fun pretty_abbrev (c, (ty, t)) = Pretty.block
     2.7 -      (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
     2.8 +      (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
     2.9  
    2.10      fun pretty_axm (a, t) =
    2.11        Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
     3.1 --- a/src/Pure/primitive_defs.ML	Sun Dec 18 12:34:31 2016 +0100
     3.2 +++ b/src/Pure/primitive_defs.ML	Sun Dec 18 13:07:13 2016 +0100
     3.3 @@ -34,7 +34,7 @@
     3.4        commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
     3.5      val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
     3.6  
     3.7 -    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
     3.8 +    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
     3.9      val lhs = Envir.beta_eta_contract raw_lhs;
    3.10      val (head, args) = Term.strip_comb lhs;
    3.11      val head_tfrees = Term.add_tfrees head [];