diff options
| -rw-r--r-- | isa/example.ML | 4 | ||||
| -rw-r--r-- | isa/example.thy | 4 |
2 files changed, 2 insertions, 6 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"; - diff --git a/isa/example.thy b/isa/example.thy index 4e0ac963..37c21578 100644 --- a/isa/example.thy +++ b/isa/example.thy @@ -7,6 +7,4 @@ *) -example = HOL - - +example = Main |