--- a/src/Pure/Isar/overloading.ML Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/Isar/overloading.ML Sun Dec 18 13:07:13 2016 +0100
@@ -139,7 +139,7 @@
| NONE => NONE);
val unchecks =
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
- in
+ in
ctxt
|> map_improvable_syntax (K {primary_constraints = [],
secondary_constraints = [], improve = K NONE, subst = subst,
@@ -168,7 +168,7 @@
val overloading = get_overloading lthy;
fun pr_operation ((c, ty), (v, _)) =
Pretty.block (Pretty.breaks
- [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
+ [Pretty.str v, Pretty.str "\<equiv>", Proof_Context.pretty_const lthy c,
Pretty.str "::", Syntax.pretty_typ lthy ty]);
in
[Pretty.block
--- a/src/Pure/Isar/proof_display.ML Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/Isar/proof_display.ML Sun Dec 18 13:07:13 2016 +0100
@@ -95,7 +95,7 @@
val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
fun pretty_abbrev (c, (ty, t)) = Pretty.block
- (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
+ (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
fun pretty_axm (a, t) =
Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
--- a/src/Pure/primitive_defs.ML Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/primitive_defs.ML Sun Dec 18 13:07:13 2016 +0100
@@ -34,7 +34,7 @@
commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
- val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
+ val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
val lhs = Envir.beta_eta_contract raw_lhs;
val (head, args) = Term.strip_comb lhs;
val head_tfrees = Term.add_tfrees head [];