equal
deleted
inserted
replaced
8 |
8 |
9 lemma "True" by normalization |
9 lemma "True" by normalization |
10 lemma "p \<longrightarrow> True" by normalization |
10 lemma "p \<longrightarrow> True" by normalization |
11 declare disj_assoc [code nbe] |
11 declare disj_assoc [code nbe] |
12 lemma "((P | Q) | R) = (P | (Q | R))" by normalization |
12 lemma "((P | Q) | R) = (P | (Q | R))" by normalization |
13 declare disj_assoc [code del] |
|
14 lemma "0 + (n::nat) = n" by normalization |
13 lemma "0 + (n::nat) = n" by normalization |
15 lemma "0 + Suc n = Suc n" by normalization |
14 lemma "0 + Suc n = Suc n" by normalization |
16 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization |
15 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization |
17 lemma "~((0::nat) < (0::nat))" by normalization |
16 lemma "~((0::nat) < (0::nat))" by normalization |
18 |
17 |