diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-08-03 20:56:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-08-03 20:56:03 +0000 |
| commit | fecfbc2d70ab83e3a8dff28229359dc8998fc2d7 (patch) | |
| tree | 23eb4e753bd4b21c7cd7741fa2c27ee16c34c6cb /isar/Example-Tokens.thy | |
| parent | da094b7fea3e69e7d1cbcae8d75263e95127b7ad (diff) | |
Fix tokens
Diffstat (limited to 'isar/Example-Tokens.thy')
| -rw-r--r-- | isar/Example-Tokens.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy index 2eee4f18..d9e5ca4d 100644 --- a/isar/Example-Tokens.thy +++ b/isar/Example-Tokens.thy @@ -12,7 +12,7 @@ text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *} theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>" proof - assume "\<phi> \<and> \<psi>" + assume "\<phi> \<and> \<psi>" then show "\<psi> \<and> \<phi>" proof assume \<psi> and \<phi> @@ -22,7 +22,7 @@ qed text {* \<^bbold>Unstructured\<^ebold> proof script. *} -theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> (\<phi>\<^isub>\<beta> ∧ \<phi>\<^isub>\<alpha>)" +theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> \<phi>\<^isub>\<beta> \<and> \<phi>\<^isub>\<alpha>" apply (rule impI) apply (erule conjE) apply (rule conjI) |