example.ML « isa - proof-general - Emacs plugins for proof management systems

about summary refs log tree commit diff

path: root/isa/example.ML

blob: 2357ef559f0644b708627a5c016b2448d61d09e2 (plain)

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