--- 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
--- 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"