diff options
Diffstat (limited to 'isa/example.ML')
| -rw-r--r-- | isa/example.ML | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/isa/example.ML b/isa/example.ML index 2357ef55..d5ba5153 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -1,4 +1,15 @@ -goal HOL.thy "(A & B)-->(B & A)"; +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"; + +goal HOL.thy + "(A & B)-->(B & A)"; br impI 1; br conjI 1; be conjE 1; |