--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Feb 25 19:30:55 2018 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Feb 25 19:43:38 2018 +0100
@@ -472,7 +472,7 @@
one of the premises. Unfortunately, this sometimes yields "Variable
has two distinct types" errors. To avoid this, we instantiate the
variables before applying "assume_tac". Typical constraints are of the form
- ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
+ ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \<equiv>\<^sup>? SK_a_b_c_x,
where the nonvariables are goal parameters. *)
fun unify_first_prem_with_concl ctxt i th =
let
--- a/src/Pure/more_thm.ML Sun Feb 25 19:30:55 2018 +0100
+++ b/src/Pure/more_thm.ML Sun Feb 25 19:43:38 2018 +0100
@@ -705,7 +705,7 @@
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
fun pretty_flexpair ctxt (t, u) = Pretty.block
- [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+ [Syntax.pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, Syntax.pretty_term ctxt u];
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
let
--- a/src/Pure/unify.ML Sun Feb 25 19:30:55 2018 +0100
+++ b/src/Pure/unify.ML Sun Feb 25 19:43:38 2018 +0100
@@ -243,7 +243,7 @@
(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs
Does not perform assignments for flex-flex pairs:
may create nonrigid paths, which prevent other assignments.
- Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
+ Does not even identify Vars in dpairs such as ?a \<equiv>\<^sup>? ?b; an attempt to
do so caused numerous problems with no compensating advantage.
*)
fun SIMPL0 context dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
@@ -426,7 +426,7 @@
(*If an argument contains a banned Bound, then it should be deleted.
But if the only path is flexible, this is difficult; the code gives up!
- In \<lambda>x y. ?a x =?= \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
+ In \<lambda>x y. ?a x \<equiv>\<^sup>? \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
exception CHANGE_FAIL; (*flexible occurrence of banned variable, or other reason to quit*)
@@ -580,7 +580,7 @@
val ctxt = Context.proof_of context;
fun termT t =
Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
- val prt = Pretty.blk (0, [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]);
+ val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
in tracing (Pretty.string_of prt) end;
in tracing msg; List.app pdp dpairs end
else ();