src/HOL/Bali/Basis.thy
 changeset 34915 7894c7dab132 parent 33965 f57c11db4ad4 child 35067 af4c18c30593
```     1.1 --- a/src/HOL/Bali/Basis.thy	Sun Jan 10 18:41:07 2010 +0100
1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Jan 10 18:43:45 2010 +0100
1.3 @@ -1,7 +1,5 @@
1.4  (*  Title:      HOL/Bali/Basis.thy
1.5 -    ID:         \$Id\$
1.6      Author:     David von Oheimb
1.7 -
1.8  *)
1.9  header {* Definitions extending HOL as logical basis of Bali *}
1.10
1.11 @@ -66,8 +64,6 @@
1.12   "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk>
1.13   \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
1.14  proof -
1.15 -  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
1.16 -  note converse_rtranclE = converse_rtranclE [consumes 1]
1.17    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
1.18    assume "(a,x)\<in>r\<^sup>*"
1.19    then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
1.20 @@ -110,13 +106,6 @@
1.21  apply (auto dest: rtrancl_into_trancl1)
1.22  done
1.23
1.24 -(* ### To Transitive_Closure *)
1.25 -theorems converse_rtrancl_induct
1.26 - = converse_rtrancl_induct [consumes 1,case_names Id Step]
1.27 -
1.28 -theorems converse_trancl_induct
1.29 -         = converse_trancl_induct [consumes 1,case_names Single Step]
1.30 -
1.31  (* context (theory "Set") *)
1.32  lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
1.33  by auto
```