# HG changeset patch
# User paulson
# Date 901636256 -7200
# Node ID 858da18069d759092c612b9600defe2b60aeef65
# Parent  eb5a1511a07dd4a8fe43ba05c7fb38f5689044df
Updated examples

diff -r eb5a1511a07d -r 858da18069d7 src/FOL/ex/Nat.ML
--- a/src/FOL/ex/Nat.ML	Mon Jul 27 17:38:55 1998 +0200
+++ b/src/FOL/ex/Nat.ML	Tue Jul 28 16:30:56 1998 +0200
@@ -58,8 +58,9 @@
 by (ALLGOALS (Asm_simp_tac));
 qed "add_Suc_right";
 
-val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
+(*Example used in Reference Manual, Doc/Ref/simplifier.tex*)
+val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
 by (res_inst_tac [("n","i")] induct 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps prems) 1);
+by (asm_simp_tac (simpset() addsimps [prem]) 1);
 result();
diff -r eb5a1511a07d -r 858da18069d7 src/FOL/ex/intro.ML
--- a/src/FOL/ex/intro.ML	Mon Jul 27 17:38:55 1998 +0200
+++ b/src/FOL/ex/intro.ML	Tue Jul 28 16:30:56 1998 +0200
@@ -12,9 +12,11 @@
 *)
 
 
+context FOL.thy;
+
 (**** Some simple backward proofs ****)
 
-goal FOL.thy "P|P --> P";
+Goal "P|P --> P";
 by (rtac impI 1);
 by (rtac disjE 1);
 by (assume_tac 3);
@@ -22,7 +24,7 @@
 by (assume_tac 1);
 qed "mythm";
 
-goal FOL.thy "(P & Q) | R  --> (P | R)";
+Goal "(P & Q) | R  --> (P | R)";
 by (rtac impI 1);
 by (etac disjE 1);
 by (dtac conjunct1 1);
@@ -32,7 +34,7 @@
 result();
 
 (*Correct version, delaying use of "spec" until last*)
-goal FOL.thy "(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
+Goal "(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
 by (rtac impI 1);
 by (rtac allI 1);
 by (rtac allI 1);
@@ -44,12 +46,12 @@
 
 (**** Demonstration of Fast_tac ****)
 
-goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
+Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
 \       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
 by (Fast_tac 1);
 result();
 
-goal FOL.thy "ALL x. P(x,f(x)) <-> \
+Goal "ALL x. P(x,f(x)) <-> \
 \       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
 by (Fast_tac 1);
 result();
@@ -57,7 +59,7 @@
 
 (**** Derivation of conjunction elimination rule ****)
 
-val [major,minor] = goal FOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R";
+val [major,minor] = Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
 by (rtac minor 1);
 by (resolve_tac [major RS conjunct1] 1);
 by (resolve_tac [major RS conjunct2] 1);
@@ -69,7 +71,7 @@
 
 (** Derivation of negation introduction **)
 
-val prems = goal FOL.thy "(P ==> False) ==> ~P";
+val prems = Goal "(P ==> False) ==> ~P";
 by (rewtac not_def);
 by (rtac impI 1);
 by (resolve_tac prems 1);
@@ -83,7 +85,7 @@
 by (rtac minor 1);
 result();
 
-(*Alternative proof of above result*)
+(*Alternative proof of the result above*)
 val [major,minor] = goalw FOL.thy [not_def]
     "[| ~P;  P |] ==> R";
 by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);