| changeset 16417 | 9bc16273c2d4 |
| parent 13756 | 41abb61ecce9 |
| child 32833 | f3716d1a2e48 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Basic = Main: |
2 theory Basic imports Main begin |
3 |
3 |
4 lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)" |
4 lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)" |
5 apply (rule conjI) |
5 apply (rule conjI) |
6 apply assumption |
6 apply assumption |
7 apply (rule conjI) |
7 apply (rule conjI) |