src/HOL/Bali/Basis.thy
changeset 12925 99131847fb93
parent 12919 d6a0d168291e
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Feb 21 20:11:32 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Feb 22 11:26:44 2002 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  done
     1.5  
     1.6  syntax
     1.7 -  "3" :: nat   ("3")
     1.8 +  "3" :: nat   ("3") 
     1.9    "4" :: nat   ("4")
    1.10  translations
    1.11   "3" == "Suc 2"
    1.12 @@ -75,7 +75,7 @@
    1.13  by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)
    1.14  
    1.15  lemma rtrancl_into_trancl3:
    1.16 -"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+"
    1.17 +"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+" 
    1.18  apply (drule rtranclD)
    1.19  apply auto
    1.20  done