1.1 --- a/src/CTT/ex/elim.ML	Thu Mar 17 12:56:44 1994 +0100
     1.2 +++ b/src/CTT/ex/elim.ML	Thu Mar 17 13:07:48 1994 +0100
     1.3 @@ -64,10 +64,11 @@
     1.4  result();
     1.5  
     1.6  (*more general goal with same proof*)
     1.7 -val prems = goal CTT.thy  
     1.8 -    "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A. B(x)) ==> C(z) type|] \
     1.9 -\    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
    1.10 -\         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
    1.11 +val prems = goal CTT.thy
    1.12 +    "[| A type; !!x. x:A ==> B(x) type; 			\
    1.13 +\               !!z. z: (SUM x:A. B(x)) ==> C(z) type 		\
    1.14 +\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
    1.15 +\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
    1.16  by (pc_tac prems 1);
    1.17  result();
    1.18  
    1.19 @@ -130,10 +131,10 @@
    1.20  (*Martin-Lof (1984) page 50*)
    1.21  writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
    1.22  val prems = goal CTT.thy   
    1.23 -    "[| A type;  !!x. x:A ==> B(x) type;  \
    1.24 -\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|]  \
    1.25 -\    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
    1.26 -\            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    1.27 +    "[| A type;  !!x. x:A ==> B(x) type;  			\
    1.28 +\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  		\
    1.29 +\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).   	\
    1.30 +\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    1.31  by (intr_tac prems);
    1.32  by (add_mp_tac 2);
    1.33  by (add_mp_tac 1);
    1.34 @@ -147,10 +148,10 @@
    1.35  
    1.36  writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
    1.37  val prems = goal CTT.thy   
    1.38 -    "[| A type;  !!x.x:A ==> B(x) type;  \
    1.39 -\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|] \
    1.40 -\    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y)) \
    1.41 -\            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    1.42 +    "[| A type;  !!x.x:A ==> B(x) type; 			\
    1.43 +\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type		\
    1.44 +\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    	\
    1.45 +\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    1.46  by (intr_tac prems);
    1.47  (*Must not use add_mp_tac as subst_prodE hides the construction.*)
    1.48  by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);