aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/Example.thy
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-12-03 00:26:21 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-12-03 00:26:21 +0000
commit304cf41b762c57bda2f1176fc8c366e9801015d2 (patch)
treeb157287d714c3e04420cba21be1442246752d555 /isar/Example.thy
parente19e6d8c98141f52852eb84eb222a524a82481e2 (diff)
Change of type for proof-script-span-context-menu-extensions
Diffstat (limited to 'isar/Example.thy')
-rw-r--r--isar/Example.thy2
1 files changed, 2 insertions, 0 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..a826cae8 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -19,6 +19,8 @@ proof
qed
qed
+(* quite nice I think but what if I type here? *)
+
text {* Unstructured proof script. *}
theorem "A & B --> B & A"