diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1999-09-13 14:03:38 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1999-09-13 14:03:38 +0000 |
commit | 0606a0391305da5a3a87bebcef15d3cf2a66be6c (patch) | |
tree | 58c64d714873d58f8128e5f37934db8301486908 /lego/example.l | |
parent | 170e4842b1f8d9975588162a7e63985d53921022 (diff) |
Cleaned up example files so all demonstrate same theorem "conj_comms".
Would be nice to add more theorems to compare scripts in different
systems.
Diffstat (limited to 'lego/example.l')
-rw-r--r-- | lego/example.l | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lego/example.l b/lego/example.l index 52643424..4a506990 100644 --- a/lego/example.l +++ b/lego/example.l @@ -1,3 +1,9 @@ +(* + Example proof script for Lego Proof General. + + $Id$ +*) + Module example Import lib_logic; Goal and_commutes: {A,B:Prop}(and A B) -> (and B A); |