src/HOL/MetisExamples/TransClosure.thy
changeset 28592 824f8390aaa2
parent 28486 873726bdfd47
child 32864 a226f29d4bdc
     1.1 --- a/src/HOL/MetisExamples/TransClosure.thy	Tue Oct 14 15:45:46 2008 +0200
     1.2 +++ b/src/HOL/MetisExamples/TransClosure.thy	Tue Oct 14 16:01:36 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5  consts f:: "addr \<Rightarrow> val"
     1.6  
     1.7 -ML {*AtpThread.problem_name := "TransClosure__test"*}
     1.8 +ML {*AtpWrapper.problem_name := "TransClosure__test"*}
     1.9  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.10     \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"  
    1.11  by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
    1.12 @@ -51,7 +51,7 @@
    1.13    by (metis 10 3)
    1.14  qed
    1.15  
    1.16 -ML {*AtpThread.problem_name := "TransClosure__test_simpler"*}
    1.17 +ML {*AtpWrapper.problem_name := "TransClosure__test_simpler"*}
    1.18  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.19     \<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
    1.20  apply (erule_tac x="b" in converse_rtranclE)