# HG changeset patch
# User lcp
# Date 763906068 -3600
# Node ID f1f96b9e6285374cfdc63705119f68967256502c
# Parent  fb379160f4deed4625cb564cceafbcf364e211a6
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
h:X.Y to fix the variable name h:X.

diff -r fb379160f4de -r f1f96b9e6285 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Thu Mar 17 12:56:44 1994 +0100
+++ b/src/CTT/ex/elim.ML	Thu Mar 17 13:07:48 1994 +0100
@@ -64,10 +64,11 @@
 result();
 
 (*more general goal with same proof*)
-val prems = goal CTT.thy  
-    "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A. B(x)) ==> C(z) type|] \
-\    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
-\         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
+val prems = goal CTT.thy
+    "[| A type; !!x. x:A ==> B(x) type; 			\
+\               !!z. z: (SUM x:A. B(x)) ==> C(z) type 		\
+\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
+\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
 by (pc_tac prems 1);
 result();
 
@@ -130,10 +131,10 @@
 (*Martin-Lof (1984) page 50*)
 writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
 val prems = goal CTT.thy   
-    "[| A type;  !!x. x:A ==> B(x) type;  \
-\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|]  \
-\    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
-\            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
+    "[| A type;  !!x. x:A ==> B(x) type;  			\
+\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  		\
+\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).   	\
+\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
 by (intr_tac prems);
 by (add_mp_tac 2);
 by (add_mp_tac 1);
@@ -147,10 +148,10 @@
 
 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
 val prems = goal CTT.thy   
-    "[| A type;  !!x.x:A ==> B(x) type;  \
-\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|] \
-\    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y)) \
-\            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
+    "[| A type;  !!x.x:A ==> B(x) type; 			\
+\       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type		\
+\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    	\
+\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
 by (intr_tac prems);
 (*Must not use add_mp_tac as subst_prodE hides the construction.*)
 by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);