diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-09-03 21:46:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-09-03 21:46:29 +0000 |
| commit | a6df07141665078a6f090a4dd20571fb9c0a68fd (patch) | |
| tree | 72ba1f6f4819d6c6834167a99a317dd3360a85d4 /isa/Example.ML | |
| parent | 96a4bbd4d51fdf065ceb983d47f4303b43b8eb08 (diff) | |
Accidental commit; revert to original.
Diffstat (limited to 'isa/Example.ML')
| -rw-r--r-- | isa/Example.ML | 122 |
1 files changed, 0 insertions, 122 deletions
diff --git a/isa/Example.ML b/isa/Example.ML index b1ad1ee2..4ef88eaa 100644 --- a/isa/Example.ML +++ b/isa/Example.ML @@ -13,125 +13,3 @@ Goal "A & B --> B & A"; qed "and_comms"; -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms2"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms3"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms8"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms3"; - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms3"; - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms3"; - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms"; - - -Goal "A & B --> B & A"; - by (rtac impI 1); - by (etac conjE 1); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); -qed "and_comms3"; - |