| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 11:02:32 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 37906 | e2b23ba9df13 |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
theory Test imports Main begin; |
| neuper@37906 | 2 |
theorem my_thm: " A & B --> B & A"; |
| neuper@37906 | 3 |
proof; |
| neuper@37906 | 4 |
assume " A & B"; |
| neuper@37906 | 5 |
then obtain B and A ..; |
| neuper@37906 | 6 |
then show "B & A" ..; |
| neuper@37906 | 7 |
qed; |