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