diff options
| author | David Aspinall | 2006-12-05 12:49:56 +0000 |
|---|---|---|
| committer | David Aspinall | 2006-12-05 12:49:56 +0000 |
| commit | 7077e2e8fed4a52af4894954c8446781cb5d40d6 (patch) | |
| tree | 023224bae2e0e278d99e94bba2f0d3fe98984495 /isa/Example.ML | |
| parent | 1ea338cca92204c9a98a373adb80ab60c3a10107 (diff) | |
Deleted file
Diffstat (limited to 'isa/Example.ML')
| -rw-r--r-- | isa/Example.ML | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/isa/Example.ML b/isa/Example.ML deleted file mode 100644 index 57733a48..00000000 --- a/isa/Example.ML +++ /dev/null @@ -1,18 +0,0 @@ -(* -*- isa -*- - - Example proof script for Isabelle Proof General. - - $Id$ - - The line at the top of this comment forces - Proof General's classic Isabelle mode - (instead of Isar: you can't use both at once). -*) - -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"; |
