diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-09-24 16:01:52 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-09-24 16:01:52 +0000 |
| commit | 7e4fd2210f230faf4f8f254cf8f1c491f3477a09 (patch) | |
| tree | 616e291674807eb419e0e231da3c7ae558a438b8 /isar/Example.thy | |
| parent | 6189e10da761f1d63135efa068cc428454e069f2 (diff) | |
tuned;
Diffstat (limited to 'isar/Example.thy')
| -rw-r--r-- | isar/Example.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 2b9c72f6..0f23f5d4 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -12,8 +12,8 @@ proof; assume "A & B"; thus "B & A"; proof; - assume B A; - thus ?thesis; ..; + assume A B; + show ?thesis; ..; qed; qed; |