--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 26 21:08:32 2017 +0100
@@ -142,7 +142,7 @@
map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE
handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
-val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
+val eq_imp_rel = @{lemma "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" by (simp add: equivp_reflp)}
fun eq_imp_rel_get ctxt =
map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
@@ -569,10 +569,10 @@
the Quot_True premise in 2nd records the lifted theorem
*)
val procedure_thm =
- @{lemma "[|A;
- A --> B;
- Quot_True D ==> B = C;
- C = D|] ==> D"
+ @{lemma "\<lbrakk>A;
+ A \<longrightarrow> B;
+ Quot_True D \<Longrightarrow> B = C;
+ C = D\<rbrakk> \<Longrightarrow> D"
by (simp add: Quot_True_def)}
(* in case of partial equivalence relations, this form of the