diff options
| author | David Aspinall | 1998-10-20 10:31:58 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-20 10:31:58 +0000 |
| commit | 13cd8eac3946221fdb51d4cb6749eac2af82555b (patch) | |
| tree | 23c3cc78c4ca4467397a3d3186deadae41e93ba1 /isa/example.ML | |
| parent | 3e0b31278ebb31d5f4b16da3c969154d85a709e3 (diff) | |
Removed duplicate proof
Diffstat (limited to 'isa/example.ML')
| -rw-r--r-- | isa/example.ML | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/isa/example.ML b/isa/example.ML index 5a6f7dfb..a8922e87 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -17,12 +17,3 @@ be conjE 1; ba 1; qed "and_comms"; -goal HOL.thy - "(A & B)-->(B & A)"; -br impI 1; -br conjI 1; -be conjE 1; -ba 1; -be conjE 1; -ba 1; -qed "and_comms"; |