# HG changeset patch
# User paulson
# Date 822099611 -3600
# Node ID a8387e934fa71f94efc5d2af2a402ebcdd992d98
# Parent  887e9816eea468c371050e86d33053ddb84f8306
Ran expandshort

diff -r 887e9816eea4 -r a8387e934fa7 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Fri Jan 19 16:00:22 1996 +0100
+++ b/src/CTT/ex/elim.ML	Sat Jan 20 02:00:11 1996 +0100
@@ -1,10 +1,10 @@
-(*  Title: 	CTT/ex/elim
+(*  Title:      CTT/ex/elim
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 Some examples taken from P. Martin-L\"of, Intuitionistic type theory
-	(Bibliopolis, 1984).
+        (Bibliopolis, 1984).
 
 by (safe_tac prems 1);
 by (step_tac prems 1);
@@ -65,9 +65,9 @@
 
 (*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 f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
+    "[| 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();
@@ -131,9 +131,9 @@
 (*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 h: (PROD x:A. SUM y:B(x). C(x,y)).   	\
+    "[| 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);
@@ -148,9 +148,9 @@
 
 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 h: (PROD x:A. SUM y:B(x). C(x,y)).    	\
+    "[| 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.*)
diff -r 887e9816eea4 -r a8387e934fa7 src/FOLP/ex/intro.ML
--- a/src/FOLP/ex/intro.ML	Fri Jan 19 16:00:22 1996 +0100
+++ b/src/FOLP/ex/intro.ML	Sat Jan 20 02:00:11 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/ex/intro
+(*  Title:      FOL/ex/intro
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 Examples for the manual "Introduction to Isabelle"
@@ -15,29 +15,29 @@
 (**** Some simple backward proofs ****)
 
 goal FOLP.thy "?p:P|P --> P";
-by (resolve_tac [impI] 1);
-by (resolve_tac [disjE] 1);
+by (rtac impI 1);
+by (rtac disjE 1);
 by (assume_tac 3);
 by (assume_tac 2);
 by (assume_tac 1);
 val mythm = result();
 
 goal FOLP.thy "?p:(P & Q) | R  --> (P | R)";
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
-by (dresolve_tac [conjunct1] 1);
-by (resolve_tac [disjI1] 1);
-by (resolve_tac [disjI2] 2);
+by (rtac impI 1);
+by (etac disjE 1);
+by (dtac conjunct1 1);
+by (rtac disjI1 1);
+by (rtac disjI2 2);
 by (REPEAT (assume_tac 1));
 result();
 
 (*Correct version, delaying use of "spec" until last*)
 goal FOLP.thy "?p:(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [allI] 1);
-by (dresolve_tac [spec] 1);
-by (dresolve_tac [spec] 1);
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac allI 1);
+by (dtac spec 1);
+by (dtac spec 1);
 by (assume_tac 1);
 result();
 
@@ -58,7 +58,7 @@
 (**** Derivation of conjunction elimination rule ****)
 
 val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
 by (resolve_tac [major RS conjunct1] 1);
 by (resolve_tac [major RS conjunct2] 1);
 prth (topthm());
@@ -70,17 +70,17 @@
 (** Derivation of negation introduction **)
 
 val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
-by (rewrite_goals_tac [not_def]);
-by (resolve_tac [impI] 1);
+by (rewtac not_def);
+by (rtac impI 1);
 by (resolve_tac prems 1);
 by (assume_tac 1);
 result();
 
 val [major,minor] = goal FOLP.thy "[| p:~P;  q:P |] ==> ?p:R";
-by (resolve_tac [FalseE] 1);
-by (resolve_tac [mp] 1);
+by (rtac FalseE 1);
+by (rtac mp 1);
 by (resolve_tac [rewrite_rule [not_def] major] 1);
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
 result();
 
 (*Alternative proof of above result*)