diff options
| author | Makarius Wenzel | 1999-08-06 18:01:09 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-08-06 18:01:09 +0000 |
| commit | cd6c2b24c5b81465d3dbcc292b4457ed37ab9fb1 (patch) | |
| tree | f4b196198273bbc1c02a92702418e717be232c2d /isa/example.ML | |
| parent | 7cc5024441ea29b5e341d0db2b04426b391da60a (diff) | |
tuned;
Diffstat (limited to 'isa/example.ML')
| -rw-r--r-- | isa/example.ML | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/isa/example.ML b/isa/example.ML index a8922e87..8ea12dfd 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -7,8 +7,7 @@ *) -goal HOL.thy - "(A & B)-->(B & A)"; +Goal "(A & B)-->(B & A)"; br impI 1; br conjI 1; be conjE 1; @@ -16,4 +15,3 @@ ba 1; be conjE 1; ba 1; qed "and_comms"; - |