src/HOL/List.thy

         and f_nth: "\<And>i. i < size [x] \<Longrightarrow> [x]!i = ys!(f i)"
       by blast
 
     have "length ys = card (f ` {0 ..< size [x]})"
       using f_img by auto
-    then have "length ys = 1" by auto
-    moreover
+    then have *: "length ys = 1" by auto
     then have "f 0 = 0" using f_img by auto
-    ultimately show ?case using f_nth by (cases ys) auto
+    with * show ?case using f_nth by (cases ys) auto
   next
     case (3 x1 x2 xs)
     from "3.prems" obtain f where f_mono: "mono f"
       and f_img: "f ` {0..<length (x1 # x2 # xs)} = {0..<length ys}"
       and f_nth:

       unfolding cs as bs by auto
     ultimately show ?thesis using n n' unfolding lexn_conv by auto
   next
     let ?k = "length abs"
     case eq
-    hence "abs = bcs" "b = b'" using bs bs' by auto
-    moreover hence "(a, c') \<in> r"
+    hence *: "abs = bcs" "b = b'" using bs bs' by auto
+    hence "(a, c') \<in> r"
       using abr b'c'r assms unfolding trans_def by blast
-    ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+    with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
   qed
 qed
 
 lemma lex_conv:
   "lex r =

 
 lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
-  moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
-  ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
+  hence "\<not> lexordp_eq ys xs" by induct simp_all
+  with \<open>?lhs\<close> show ?rhs by (simp add: lexordp_into_lexordp_eq)
 next
   assume ?rhs
   hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
   thus ?lhs by induct simp_all
 qed