--- a/src/HOL/Metis_Examples/Sets.thy Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Tue Nov 06 15:15:33 2012 +0100
@@ -21,7 +21,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
(*multiple versions of this example*)
lemma (*equal_union: *)
@@ -70,7 +70,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proofs, isar_shrinkage = 2]
+sledgehammer_params [isar_proofs, isar_shrink = 2]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -107,7 +107,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proofs, isar_shrinkage = 3]
+sledgehammer_params [isar_proofs, isar_shrink = 3]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -124,7 +124,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
qed
-sledgehammer_params [isar_proofs, isar_shrinkage = 4]
+sledgehammer_params [isar_proofs, isar_shrink = 4]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -140,7 +140,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
qed
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"