diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-09 15:58:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-09 15:58:29 +0000 |
| commit | 58b9e2ceeca8079d139ee1c0d8e5653ba69a403f (patch) | |
| tree | d27a58b828014b0f3e4f531a224cac1b7871d17b /isa | |
| parent | cff1ff992342a410e7e4ec248aaa34f59eee09b3 (diff) | |
New goal.
Diffstat (limited to 'isa')
| -rw-r--r-- | isa/Example.ML | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/isa/Example.ML b/isa/Example.ML index bf5ee3f0..673f7c6f 100644 --- a/isa/Example.ML +++ b/isa/Example.ML @@ -12,4 +12,6 @@ by (assume_tac 1); by (assume_tac 1); qed "and_comms"; -Goal "P(x) --> Q(x)"; +Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)"; + + |