src/HOL/ex/Groebner_Examples.thy
changeset 36319 8feb2c4bef1a
parent 31021 53642251a04f
child 36700 9b85b9d74b83
--- a/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -10,13 +10,13 @@
 
 subsection {* Basic examples *}
 
-lemma "3 ^ 3 == (?X::'a::{number_ring})"
+schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
   by sring_norm
 
-lemma "(x - (-2))^5 == ?X::int"
+schematic_lemma "(x - (-2))^5 == ?X::int"
   by sring_norm
 
-lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
+schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
   by sring_norm
 
 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"