--- a/src/FOLP/ex/intro.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/intro.ML Sun Sep 18 14:25:48 2005 +0200
@@ -14,7 +14,7 @@
(**** Some simple backward proofs ****)
-goal FOLP.thy "?p:P|P --> P";
+goal (theory "FOLP") "?p:P|P --> P";
by (rtac impI 1);
by (rtac disjE 1);
by (assume_tac 3);
@@ -22,7 +22,7 @@
by (assume_tac 1);
val mythm = result();
-goal FOLP.thy "?p:(P & Q) | R --> (P | R)";
+goal (theory "FOLP") "?p:(P & Q) | R --> (P | R)";
by (rtac impI 1);
by (etac disjE 1);
by (dtac conjunct1 1);
@@ -32,7 +32,7 @@
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))";
+goal (theory "FOLP") "?p:(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 +44,12 @@
(**** Demonstration of fast_tac ****)
-goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x)) \
+goal (theory "FOLP") "?p:(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 FOLP_cs 1);
result();
-goal FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
+goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
\ (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
by (fast_tac FOLP_cs 1);
result();
@@ -57,7 +57,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";
+val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
by (rtac minor 1);
by (resolve_tac [major RS conjunct1] 1);
by (resolve_tac [major RS conjunct2] 1);
@@ -69,14 +69,14 @@
(** Derivation of negation introduction **)
-val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
+val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
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";
+val [major,minor] = goal (theory "FOLP") "[| p:~P; q:P |] ==> ?p:R";
by (rtac FalseE 1);
by (rtac mp 1);
by (resolve_tac [rewrite_rule [not_def] major] 1);
@@ -84,9 +84,7 @@
result();
(*Alternative proof of above result*)
-val [major,minor] = goalw FOLP.thy [not_def]
+val [major,minor] = goalw (theory "FOLP") [not_def]
"[| p:~P; q:P |] ==> ?p:R";
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
result();
-
-writeln"Reached end of file.";