diff options
| author | David Aspinall | 1998-09-09 14:02:46 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-09-09 14:02:46 +0000 |
| commit | f45e4719e7e78d27566cb141f48afccca1e3fd06 (patch) | |
| tree | b1c60befcda607743a068397b03dcb20aceaf952 /isa/example.ML | |
| parent | a4c0501d4007ad5f2d2f43c2cb5d1d5f137c6618 (diff) | |
Added Id to headers.
Diffstat (limited to 'isa/example.ML')
| -rw-r--r-- | isa/example.ML | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/isa/example.ML b/isa/example.ML index d5ba5153..5a6f7dfb 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -1,3 +1,12 @@ +(* + Example proof script for Isabelle + + David Aspinall <da@dcs.ed.ac.uk> + + $Id$ + +*) + goal HOL.thy "(A & B)-->(B & A)"; br impI 1; |