src/CCL/Wfd.thy
changeset 41526 54b4686704af
parent 38500 d5477ee35820
child 42364 8c674b3b8e44
     1.1 --- a/src/CCL/Wfd.thy	Wed Jan 12 15:53:37 2011 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Wed Jan 12 16:33:04 2011 +0100
     1.3 @@ -253,11 +253,11 @@
     1.4    shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
     1.5    apply (unfold letrec2_def)
     1.6    apply (rule SPLITB [THEN subst])
     1.7 -  apply (assumption | rule letrecT pairT splitT prems)+
     1.8 +  apply (assumption | rule letrecT pairT splitT assms)+
     1.9    apply (subst SPLITB)
    1.10 -  apply (assumption | rule ballI SubtypeI prems)+
    1.11 +  apply (assumption | rule ballI SubtypeI assms)+
    1.12    apply (rule SPLITB [THEN subst])
    1.13 -  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
    1.14 +  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
    1.15      erule bspec SubtypeE sym [THEN subst])+
    1.16    done
    1.17  
    1.18 @@ -275,11 +275,11 @@
    1.19    shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
    1.20    apply (unfold letrec3_def)
    1.21    apply (rule lem [THEN subst])
    1.22 -  apply (assumption | rule letrecT pairT splitT prems)+
    1.23 +  apply (assumption | rule letrecT pairT splitT assms)+
    1.24    apply (simp add: SPLITB)
    1.25 -  apply (assumption | rule ballI SubtypeI prems)+
    1.26 +  apply (assumption | rule ballI SubtypeI assms)+
    1.27    apply (rule lem [THEN subst])
    1.28 -  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
    1.29 +  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
    1.30      erule bspec SubtypeE sym [THEN subst])+
    1.31    done
    1.32  
    1.33 @@ -520,7 +520,7 @@
    1.34    assumes "f ---> lam x. b(x)"
    1.35      and "b(a) ---> c"
    1.36    shows "f ` a ---> c"
    1.37 -  unfolding apply_def by (eval prems)
    1.38 +  unfolding apply_def by (eval assms)
    1.39  
    1.40  lemma letV:
    1.41    assumes 1: "t ---> a"