# HG changeset patch
# User wenzelm
# Date 1464010178 -7200
# Node ID 6813818baa6713410b3a079c8416c755b8fa4ced
# Parent  caa0c513bbca08d8147fdd2909325b750d3f8959
tuned proofs;

diff -r caa0c513bbca -r 6813818baa67 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 14:56:48 2016 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 15:29:38 2016 +0200
@@ -800,8 +800,8 @@
   assumes iseq: "idx_sequence idx"
     and eq: "idx m = idx n"
   shows "m = n"
-proof (rule nat_less_cases)
-  assume "n<m"
+proof (cases m n rule: linorder_cases)
+  case greater
   then obtain k where "m = Suc(n+k)"
     by (auto simp add: less_iff_Suc_add)
   with iseq have "idx n < idx m"
@@ -809,14 +809,14 @@
   with eq show ?thesis
     by simp
 next
-  assume "m<n"
+  case less
   then obtain k where "n = Suc(m+k)"
     by (auto simp add: less_iff_Suc_add)
   with iseq have "idx m < idx n"
     by (simp add: idx_sequence_less)
   with eq show ?thesis
     by simp
-qed (simp)
+qed
 
 lemma idx_sequence_mono:
   assumes iseq: "idx_sequence idx"
@@ -883,8 +883,8 @@
     and k: "n \<in> {idx k ..< idx (Suc k)}"
     and m: "n \<in> {idx m ..< idx (Suc m)}"
   shows "k = m"
-proof (rule nat_less_cases)
-  assume "k < m"
+proof (cases k m rule: linorder_cases)
+  case less
   hence "Suc k \<le> m" by simp
   with iseq have "idx (Suc k) \<le> idx m"
     by (rule idx_sequence_mono)
@@ -894,7 +894,7 @@
     by simp
   thus ?thesis ..
 next
-  assume "m < k"
+  case greater
   hence "Suc m \<le> k" by simp
   with iseq have "idx (Suc m) \<le> idx k"
     by (rule idx_sequence_mono)
@@ -903,7 +903,7 @@
   with m have "False"
     by simp
   thus ?thesis ..
-qed (simp)
+qed
 
 lemma idx_sequence_unique_interval:
   assumes iseq: "idx_sequence idx"