equal
deleted
inserted
replaced
5 header {* Test of normalization function *} |
5 header {* Test of normalization function *} |
6 |
6 |
7 theory NormalForm |
7 theory NormalForm |
8 imports Main "~~/src/HOL/Real/Rational" |
8 imports Main "~~/src/HOL/Real/Rational" |
9 begin |
9 begin |
10 |
|
11 declare equals_eq [symmetric, code post] |
|
12 |
10 |
13 lemma "True" by normalization |
11 lemma "True" by normalization |
14 lemma "p \<longrightarrow> True" by normalization |
12 lemma "p \<longrightarrow> True" by normalization |
15 declare disj_assoc [code func] |
13 declare disj_assoc [code func] |
16 lemma "((P | Q) | R) = (P | (Q | R))" by normalization rule |
14 lemma "((P | Q) | R) = (P | (Q | R))" by normalization rule |