src/CTT/CTT.thy
changeset 23467 d1b97708d5eb
parent 22808 a7daa74e2980
child 26391 6e8aa5a4eb82
     1.1 --- a/src/CTT/CTT.thy	Thu Jun 21 20:48:48 2007 +0200
     1.2 +++ b/src/CTT/CTT.thy	Thu Jun 21 22:10:16 2007 +0200
     1.3 @@ -397,13 +397,13 @@
     1.4  
     1.5  (*Simplify the parameter of a unary type operator.*)
     1.6  lemma subst_eqtyparg:
     1.7 -  assumes "a=c : A"
     1.8 -    and "!!z. z:A ==> B(z) type"
     1.9 +  assumes 1: "a=c : A"
    1.10 +    and 2: "!!z. z:A ==> B(z) type"
    1.11    shows "B(a)=B(c)"
    1.12  apply (rule subst_typeL)
    1.13  apply (rule_tac [2] refl_type)
    1.14 -apply (rule prems)
    1.15 -apply assumption
    1.16 +apply (rule 1)
    1.17 +apply (erule 2)
    1.18  done
    1.19  
    1.20  (*Simplification rules for Constructive Type Theory*)