# HG changeset patch
# User wenzelm
# Date 1475411870 -7200
# Node ID 9c0ff0c1211602df74c69712aee5e50ae3acc8e7
# Parent  3aa9837d05c7ec978946fa54c23604cd99b3c784
eliminated hard tabs;

diff -r 3aa9837d05c7 -r 9c0ff0c12116 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sun Oct 02 14:07:43 2016 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Oct 02 14:37:50 2016 +0200
@@ -331,7 +331,7 @@
     assume "S \<in> \<F>"
     have "{T \<in> \<F>. S \<subseteq> T} = {}" if "~ (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
       apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
-	 using assms that apply auto
+      using assms that apply auto
       by (blast intro: dual_order.trans psubset_imp_subset)
     then show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
       using \<open>S \<in> \<F>\<close> by blast
diff -r 3aa9837d05c7 -r 9c0ff0c12116 src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Sun Oct 02 14:07:43 2016 +0200
+++ b/src/HOL/Library/Perm.thy	Sun Oct 02 14:37:50 2016 +0200
@@ -278,7 +278,7 @@
 
 definition order :: "'a perm \<Rightarrow> 'a \<Rightarrow> nat"
 where
-	"order f = card \<circ> orbit f"
+  "order f = card \<circ> orbit f"
 
 lemma orbit_subset_eq_affected:
   assumes "a \<in> affected f"