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