src/FOLP/ex/intro.ML
 changeset 1446 a8387e934fa7 parent 0 a5a9c433f639 child 1464 a608f83e3421
```--- 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

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*)```