diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Dec 30 20:30:42 2015 +0100
@@ -69,7 +69,7 @@
   
 
 lemma (in lbv) merge_mono:
-  assumes less:  "ss2 <=|r| ss1"
+  assumes less:  "ss2 \<le>|r| ss1"
   assumes x:     "x \<in> A"
   assumes ss1:   "snd`set ss1 \<subseteq> A"
   assumes ss2:   "snd`set ss2 \<subseteq> A"
@@ -131,7 +131,7 @@
   assumes s2:   "s2 \<in> A"
   shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
 proof -
-  from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD)
+  from mono pc s2 less have "step pc s2 \<le>|r| step pc s1" by (rule monoD)
   moreover
   from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3)
   moreover