more compact proof terms;

--- a/src/HOL/Enum.thy	Tue Aug 13 20:16:03 2019 +0200
+++ b/src/HOL/Enum.thy	Tue Aug 13 20:17:02 2019 +0200
@@ -696,11 +696,12 @@
 definition "sgn = (\<lambda>x :: finite_2. x)"
 instance
   by standard
-    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
-      times_finite_2_def
-      inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
-      abs_finite_2_def sgn_finite_2_def
-      split: finite_2.splits)
+    (subproofs
+      \<open>simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
+        times_finite_2_def
+        inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
+        abs_finite_2_def sgn_finite_2_def
+        split: finite_2.splits\<close>)
 end
 
 lemma two_finite_2 [simp]:
@@ -718,8 +719,9 @@
 definition [simp]: "division_segment (x :: finite_2) = 1"
 instance
   by standard
-    (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
-    split: finite_2.splits)
+    (subproofs
+      \<open>auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
+        split: finite_2.splits\<close>)
 end
 
  
@@ -930,12 +932,13 @@
 definition "sgn = (\<lambda>x :: finite_3. x)"
 instance
   by standard
-    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
-      times_finite_3_def
-      inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
-      abs_finite_3_def sgn_finite_3_def
-      less_finite_3_def
-      split: finite_3.splits)
+    (subproofs
+      \<open>simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
+        times_finite_3_def
+        inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
+        abs_finite_3_def sgn_finite_3_def
+        less_finite_3_def
+        split: finite_3.splits\<close>)
 end
 
 lemma two_finite_3 [simp]:
@@ -951,14 +954,17 @@
 definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
 definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
 definition [simp]: "division_segment (x :: finite_3) = 1"
-instance proof
+instance
+proof
   fix x :: finite_3
   assume "x \<noteq> 0"
   then show "is_unit (unit_factor x)"
     by (cases x) (simp_all add: dvd_finite_3_unfold)
-qed (auto simp add: divide_finite_3_def times_finite_3_def
-  dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
-  split: finite_3.splits)
+qed
+  (subproofs
+    \<open>auto simp add: divide_finite_3_def times_finite_3_def
+      dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
+      split: finite_3.splits\<close>)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
@@ -1029,9 +1035,11 @@
   | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   | _ \<Rightarrow> a\<^sub>1)"
 
-instance proof
-qed(auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def 
-    inf_finite_4_def sup_finite_4_def split: finite_4.splits)
+instance
+  by standard
+    (subproofs
+      \<open>auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def 
+        inf_finite_4_def sup_finite_4_def split: finite_4.splits\<close>)
 end
 
 instance finite_4 :: complete_lattice ..
@@ -1042,9 +1050,10 @@
 definition "- x = (case x of a\<^sub>1 \<Rightarrow> a\<^sub>4 | a\<^sub>2 \<Rightarrow> a\<^sub>3 | a\<^sub>3 \<Rightarrow> a\<^sub>2 | a\<^sub>4 \<Rightarrow> a\<^sub>1)"
 definition "x - y = x \<sqinter> - (y :: finite_4)"
 instance
-by intro_classes
-  (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def 
-    split: finite_4.splits)
+  by standard
+    (subproofs
+      \<open>simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def 
+        split: finite_4.splits\<close>)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
@@ -1130,10 +1139,11 @@
    | (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
    | _ \<Rightarrow> a\<^sub>1)"
 
-instance 
-proof
-qed (auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def 
-    Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
+instance
+  by standard
+    (subproofs
+      \<open>auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def 
+        Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm\<close>)
 end