src/CTT/CTT.thy
changeset 26391 6e8aa5a4eb82
parent 23467 d1b97708d5eb
child 26956 1309a6a0a29f
equal deleted inserted replaced
26390:99d4cbb1f941 26391:6e8aa5a4eb82
   498     and "!!x. x:A ==> B(x) type"
   498     and "!!x. x:A ==> B(x) type"
   499   shows "snd(p) : B(fst(p))"
   499   shows "snd(p) : B(fst(p))"
   500   apply (unfold basic_defs)
   500   apply (unfold basic_defs)
   501   apply (rule major [THEN SumE])
   501   apply (rule major [THEN SumE])
   502   apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
   502   apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
   503   apply (tactic {* typechk_tac (thms "prems") *})
   503   apply (tactic {* typechk_tac @{thms assms} *})
   504   done
   504   done
   505 
   505 
   506 end
   506 end