diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2005-03-23 17:26:24 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2005-03-23 17:26:24 +0000 |
| commit | 8955ffee5e7b18241e1c13ab6228e64d2893f134 (patch) | |
| tree | 4a56b2fcb38d786b06dec52f525a138b1438c106 | |
| parent | 0139048d79b62b09128eabbaacd2168d32c3ae73 (diff) | |
Use another symbol
| -rw-r--r-- | isar/Example-Xsym.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy index c731143b..48661f6a 100644 --- a/isar/Example-Xsym.thy +++ b/isar/Example-Xsym.thy @@ -24,7 +24,7 @@ text {* Proper proof text -- \textit{advanced version}. *} theorem "A \<and> B \<longrightarrow> B \<and> A" proof - assume "A & B" + assume "A \<and> B" then obtain B and A .. then show "B \<and> A" .. qed |