src/HOL/ex/Groebner_Examples.thy
changeset 36319 8feb2c4bef1a
parent 31021 53642251a04f
child 36700 9b85b9d74b83
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -10,13 +10,13 @@
     1.4  
     1.5  subsection {* Basic examples *}
     1.6  
     1.7 -lemma "3 ^ 3 == (?X::'a::{number_ring})"
     1.8 +schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
     1.9    by sring_norm
    1.10  
    1.11 -lemma "(x - (-2))^5 == ?X::int"
    1.12 +schematic_lemma "(x - (-2))^5 == ?X::int"
    1.13    by sring_norm
    1.14  
    1.15 -lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
    1.16 +schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
    1.17    by sring_norm
    1.18  
    1.19  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"