equal
deleted
inserted
replaced
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Force = Main: |
2 theory Force = Divides: (*Divides rather than Main so that the first proof |
|
3 isn't done by the nat_divide_cancel_factor simprocs.*) |
3 |
4 |
|
5 declare div_mult_self_is_m [simp del]; |
|
6 |
|
7 lemma div_mult_self_is_m: |
|
8 "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
|
9 apply (insert mod_div_equality [of "m*n" n]) |
|
10 apply simp |
|
11 done |
4 |
12 |
5 |
13 |
6 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)" |
14 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)" |
7 apply clarify |
15 apply clarify |
8 oops |
16 oops |