aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/Example.thy
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2008-03-14 20:42:52 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2008-03-14 20:42:52 +0000
commit9bfd6db50aedf254d2cbbc1bb7c141f0ec986fd5 (patch)
treebb612ee8fa3536df23ccbda0b964fff02e3971d6 /isar/Example.thy
parent1705d1fecdc07d2203c2c83b5064b8150bdfe592 (diff)
proper indentation;
Diffstat (limited to 'isar/Example.thy')
-rw-r--r--isar/Example.thy3
1 files changed, 1 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 43f515ba..0fe43c25 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -14,8 +14,7 @@ proof
then show "B & A"
proof
assume B and A
- then
- show ?thesis ..
+ then show ?thesis ..
qed
qed