diff options
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)"; + + |