aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/Example.thy
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2005-03-25 12:32:18 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2005-03-25 12:32:18 +0000
commit60a0bcd3c8a15769756d470c70b53f674e58e104 (patch)
tree3addd877c9b9189fbd515d795fc48d3d1b3e6fd2 /isar/Example.thy
parent0ce9b459d94620e1be6acdd00c7f96c55ee0c44c (diff)
Remove junk
Diffstat (limited to 'isar/Example.thy')
-rw-r--r--isar/Example.thy2
1 files changed, 0 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy
index 278e5964..77a14505 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -19,8 +19,6 @@ proof
qed
qed
-asd
-
text {* Proper proof text -- \textit{advanced version}. *}
theorem "A & B --> B & A"