--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 26 21:08:32 2017 +0100
@@ -99,7 +99,7 @@
(* INFERENCE RULE: ASSUME *)
-val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
+val EXCLUDED_MIDDLE = @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
fun inst_excluded_middle ctxt i_atom =
let
@@ -256,7 +256,7 @@
don't use this trick in general because it makes the proof object uglier than
necessary. FIXME. *)
fun negate_head ctxt th =
- if exists (fn t => t aconv @{prop "~ False"}) (Thm.prems_of th) then
+ if exists (fn t => t aconv @{prop "\<not> False"}) (Thm.prems_of th) then
(th RS @{thm select_FalseI})
|> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select}
else
@@ -298,7 +298,7 @@
(* INFERENCE RULE: REFL *)
-val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by simp}
val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
@@ -312,8 +312,8 @@
(* INFERENCE RULE: EQUALITY *)
-val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
-val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
+val subst_em = @{lemma "s = t \<Longrightarrow> P s \<Longrightarrow> \<not> P t \<Longrightarrow> False" by simp}
+val ssubst_em = @{lemma "s = t \<Longrightarrow> P t \<Longrightarrow> \<not> P s \<Longrightarrow> False" by simp}
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt