src/HOL/ex/cla.ML
 changeset 5278 a903b66822e2 parent 5150 6e2e9b92c301 child 6799 95abcc002a21
```     1.1 --- a/src/HOL/ex/cla.ML	Thu Aug 06 15:47:26 1998 +0200
1.2 +++ b/src/HOL/ex/cla.ML	Thu Aug 06 15:48:13 1998 +0200
1.3 @@ -142,8 +142,7 @@
1.4  result();
1.5
1.6  (*From Wishnu Prasetya*)
1.7 -Goal
1.8 -   "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
1.9 +Goal "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
1.10  \   --> p(t) | r(t)";
1.11  by (Blast_tac 1);
1.12  result();
1.13 @@ -317,8 +316,7 @@
1.14  result();
1.15
1.16  writeln"Problem 38";
1.17 -Goal
1.18 -    "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
1.19 +Goal "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
1.20  \          (? z. ? w. p(z) & r x w & r w z))  =                 \
1.21  \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
1.22  \          (~p(a) | ~(? y. p(y) & r x y) |                      \
1.23 @@ -349,8 +347,7 @@
1.24  result();
1.25
1.26  writeln"Problem 43!!";
1.27 -Goal
1.28 -    "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
1.29 +Goal "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
1.30  \ --> (! x. (! y. q x y = (q y x::bool)))";
1.31  by (Blast_tac 1);
1.32  result();
1.33 @@ -364,8 +361,7 @@
1.34  result();
1.35
1.36  writeln"Problem 45";
1.37 -Goal
1.38 -    "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
1.39 +Goal "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
1.40  \                     --> (! y. g(y) & h x y --> k(y))) &       \
1.41  \    ~ (? y. l(y) & k(y)) &                                     \
1.42  \    (? x. f(x) & (! y. h x y --> l(y))                         \
1.43 @@ -402,16 +398,14 @@
1.44  result();
1.45
1.46  writeln"Problem 51";
1.47 -Goal
1.48 -    "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
1.49 +Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
1.50  \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
1.51  by (Blast_tac 1);
1.52  result();
1.53
1.54  writeln"Problem 52";
1.55  (*Almost the same as 51. *)
1.56 -Goal
1.57 -    "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
1.58 +Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
1.59  \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
1.60  by (Blast_tac 1);
1.61  result();
1.62 @@ -433,14 +427,12 @@
1.63  result();
1.64
1.65  writeln"Problem 56";
1.66 -Goal
1.67 -    "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
1.68 +Goal "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
1.69  by (Blast_tac 1);
1.70  result();
1.71
1.72  writeln"Problem 57";
1.73 -Goal
1.74 -    "P (f a b) (f b c) & P (f b c) (f a c) & \
1.75 +Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
1.76  \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
1.77  by (Blast_tac 1);
1.78  result();
1.79 @@ -457,8 +449,7 @@
1.80  result();
1.81
1.82  writeln"Problem 60";
1.83 -Goal
1.84 -    "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
1.85 +Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
1.86  by (Blast_tac 1);
1.87  result();
1.88
```