diff options
| -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 |