diff options
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"; |