# HG changeset patch
# User wenzelm
# Date 1634076155 -7200
# Node ID ce8152fb021bbef27ea248852f131430dffbe48f
# Parent  7422950f395551c1590eca5b424997cac0341bf0
removed junk;

diff -r 7422950f3955 -r ce8152fb021b src/HOL/Hoare/ExamplesTC.thy
--- a/src/HOL/Hoare/ExamplesTC.thy	Tue Oct 12 20:58:00 2021 +0200
+++ b/src/HOL/Hoare/ExamplesTC.thy	Wed Oct 13 00:02:35 2021 +0200
@@ -27,7 +27,7 @@
 Here is the total-correctness proof for the same program.
 It needs the additional invariant \<open>m \<le> a\<close>.
 \<close>
-ML \<open>\<^const_syntax>\<open>HOL.eq\<close>\<close>
+
 lemma multiply_by_add_tc: "VARS m s a b
   [a=A \<and> b=B]
   m := 0; s := 0;