src/CTT/ex/typechk.ML

--- a/src/CTT/ex/typechk.ML	Wed Jul 05 17:52:24 2000 +0200
+++ b/src/CTT/ex/typechk.ML	Wed Jul 05 18:27:55 2000 +0200
@@ -8,7 +8,7 @@
 
 writeln"Single-step proofs: verifying that a type is well-formed";
 
-goal CTT.thy "?A type";
+Goal "?A type";
 by (resolve_tac form_rls 1);
 result(); 
 writeln"getting a second solution";
@@ -17,7 +17,7 @@
 by (resolve_tac form_rls 1);
 result(); 
 
-goal CTT.thy "PROD z:?A . N + ?B(z) type";
+Goal "PROD z:?A . N + ?B(z) type";
 by (resolve_tac form_rls 1);
 by (resolve_tac form_rls 1);
 by (resolve_tac form_rls 1);
@@ -28,34 +28,34 @@
 
 writeln"Multi-step proofs: Type inference";
 
-goal CTT.thy "PROD w:N. N + N type";
+Goal "PROD w:N. N + N type";
 by form_tac;
 result(); 
 
-goal CTT.thy "<0, succ(0)> : ?A";
+Goal "<0, succ(0)> : ?A";
 by (intr_tac[]);
 result(); 
 
-goal CTT.thy "PROD w:N . Eq(?A,w,w) type";
+Goal "PROD w:N . Eq(?A,w,w) type";
 by (typechk_tac[]);
 result(); 
 
-goal CTT.thy "PROD x:N . PROD y:N . Eq(?A,x,y) type";
+Goal "PROD x:N . PROD y:N . Eq(?A,x,y) type";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking an application of fst";
-goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
+Goal "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the predecessor function";
-goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
+Goal "lam n. rec(n, 0, %x y. x) : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the addition function";
-goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
+Goal "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
 by (typechk_tac[]);
 result(); 
 
@@ -63,18 +63,18 @@
   For concreteness, every type variable left over is forced to be N*)
 val N_tac = TRYALL (rtac NF);
 
-goal CTT.thy "lam w. <w,w> : ?A";
+Goal "lam w. <w,w> : ?A";
 by (typechk_tac[]);
 by N_tac;
 result(); 
 
-goal CTT.thy "lam x. lam y. x : ?A";
+Goal "lam x. lam y. x : ?A";
 by (typechk_tac[]);
 by N_tac;
 result(); 
 
 writeln"typechecking fst (as a function object) ";
-goal CTT.thy "lam i. split(i, %j k. j) : ?A";
+Goal "lam i. split(i, %j k. j) : ?A";
 by (typechk_tac[]);
 by N_tac;
 result();