src/CCL/Wfd.thy
changeset 41526 54b4686704af
parent 38500 d5477ee35820
child 42364 8c674b3b8e44
--- a/src/CCL/Wfd.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/Wfd.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -253,11 +253,11 @@
   shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
   apply (unfold letrec2_def)
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (subst SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
@@ -275,11 +275,11 @@
   shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
   apply (unfold letrec3_def)
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (simp add: SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
@@ -520,7 +520,7 @@
   assumes "f ---> lam x. b(x)"
     and "b(a) ---> c"
   shows "f ` a ---> c"
-  unfolding apply_def by (eval prems)
+  unfolding apply_def by (eval assms)
 
 lemma letV:
   assumes 1: "t ---> a"