src/HOL/Library/Perm.thy

     by (auto simp add: orbit_def in_affected dest: range_eq_singletonD [of _ _ 1])
 qed
 
 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"
   shows "orbit f a \<subseteq> affected f"
 proof (rule ccontr)