equal
deleted
inserted
replaced
8 imports Groebner_Basis |
8 imports Groebner_Basis |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Basic examples *} |
11 subsection {* Basic examples *} |
12 |
12 |
13 lemma "3 ^ 3 == (?X::'a::{number_ring})" |
13 schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})" |
14 by sring_norm |
14 by sring_norm |
15 |
15 |
16 lemma "(x - (-2))^5 == ?X::int" |
16 schematic_lemma "(x - (-2))^5 == ?X::int" |
17 by sring_norm |
17 by sring_norm |
18 |
18 |
19 lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" |
19 schematic_lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" |
20 by sring_norm |
20 by sring_norm |
21 |
21 |
22 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" |
22 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" |
23 apply (simp only: power_Suc power_0) |
23 apply (simp only: power_Suc power_0) |
24 apply (simp only: comp_arith) |
24 apply (simp only: comp_arith) |