src/HOL/Bali/AxSem.thy
changeset 13585 db4005b40cc6
parent 13384 a34e38154413
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/AxSem.thy	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4    "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
     1.5  
     1.6  lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
     1.7 -apply (rule injI)
     1.8 +apply (rule inj_onI)
     1.9  apply auto
    1.10  done
    1.11