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 /isa/example.ML | |
| 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 'isa/example.ML')
| -rw-r--r-- | isa/example.ML | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/isa/example.ML b/isa/example.ML index 8ea12dfd..41ea20be 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -1,10 +1,7 @@ (* - Example proof script for Isabelle - - David Aspinall <da@dcs.ed.ac.uk> + Example proof script for Isabelle Proof General. $Id$ - *) Goal "(A & B)-->(B & A)"; |