src/HOL/Metis_Examples/Trans_Closure.thy
changeset 50020 6b9611abcd4c
parent 49918 cf441f4a358b
child 50705 0e943b33d907
     1.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:12:31 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:15:33 2012 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
     1.6         \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
     1.7 -(* sledgehammer [isar_proofs, isar_shrinkage = 2] *)
     1.8 +(* sledgehammer [isar_proofs, isar_shrink = 2] *)
     1.9  proof -
    1.10    assume A1: "f c = Intg x"
    1.11    assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"