src/CCL/typecheck.ML
 changeset 642 0db578095e6a parent 289 78541329ff35 child 757 2ca12511676d
```     1.1 --- a/src/CCL/typecheck.ML	Wed Oct 12 16:38:58 1994 +0100
1.2 +++ b/src/CCL/typecheck.ML	Wed Oct 19 09:23:56 1994 +0100
1.3 @@ -13,7 +13,7 @@
1.4  val Subtype_canTs =
1.5         let fun tac prems = cut_facts_tac prems 1 THEN
1.6                  REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
1.7 -                        eresolve_tac [SubtypeE] 1)
1.8 +                        etac SubtypeE 1)
1.9             fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
1.10         in map solve
1.11             ["P(one) ==> one : {x:Unit.P(x)}",
1.12 @@ -31,7 +31,7 @@
1.13  val Subtype_canTs =
1.14         let fun tac prems = cut_facts_tac prems 1 THEN
1.15                  REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
1.16 -                        eresolve_tac [SubtypeE] 1)
1.17 +                        etac SubtypeE 1)
1.18             fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
1.19         in map solve
1.20             ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
1.21 @@ -44,8 +44,8 @@
1.22  val prems = goal Type.thy
1.23       "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B";
1.24  by (cut_facts_tac prems 1);
1.25 -be (letB RS ssubst) 1;
1.26 -ba 1;
1.27 +by (etac (letB RS ssubst) 1);
1.28 +by (assume_tac 1);
1.29  val letT = result();
1.30
1.31  val prems = goal Type.thy
```