| changeset 16417 | 9bc16273c2d4 |
| parent 13756 | 41abb61ecce9 |
| child 32833 | f3716d1a2e48 |
--- a/doc-src/TutorialI/Rules/Basic.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/TutorialI/Rules/Basic.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,5 +1,5 @@ (* ID: $Id$ *) -theory Basic = Main: +theory Basic imports Main begin lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)" apply (rule conjI)