# HG changeset patch
# User haftmann
# Date 1315201771 -7200
# Node ID 4ea8489593402176f8c64476fb32880c0e855cc5
# Parent  f710ce327b08771e42fb7097aae4c399e29cedc3
tuned

diff -r f710ce327b08 -r 4ea848959340 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Sep 04 09:28:15 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Sep 05 07:49:31 2011 +0200
@@ -486,22 +486,9 @@
 
 end
 
-instance unit :: finite proof
-qed (simp add: UNIV_unit)
-
-instance bool :: finite proof
-qed (simp add: UNIV_bool)
-
 instance prod :: (finite, finite) finite proof
 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
 
-lemma finite_option_UNIV [simp]:
-  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
-  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
-
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
 
@@ -519,9 +506,22 @@
   qed
 qed
 
+instance bool :: finite proof
+qed (simp add: UNIV_bool)
+
+instance unit :: finite proof
+qed (simp add: UNIV_unit)
+
 instance sum :: (finite, finite) finite proof
 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
 
+lemma finite_option_UNIV [simp]:
+  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
+
+instance option :: (finite) finite proof
+qed (simp add: UNIV_option_conv)
+
 
 subsection {* A basic fold functional for finite sets *}