diff -r 226d29db8e0a -r b617ddd200eb src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Fri Jan 26 13:59:06 2007 +0100
+++ b/src/HOL/ex/ReflectionEx.thy	Sun Jan 28 11:52:52 2007 +0100
@@ -355,4 +355,38 @@
   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
 oops
 
+
+  (* An example for equations containing type variables *)	
+datatype prod = Zero | One | Var nat | Mul prod prod 
+  | Pw prod nat | PNM nat nat prod
+consts Iprod :: "('a::{ordered_idom,recpower}) list \<Rightarrow> prod \<Rightarrow> 'a" 
+primrec
+  "Iprod vs Zero = 0"
+  "Iprod vs One = 1"
+  "Iprod vs (Var n) = vs!n"
+  "Iprod vs (Mul a b) = (Iprod vs a * Iprod vs b)"
+  "Iprod vs (Pw a n) = ((Iprod vs a) ^ n)"
+  "Iprod vs (PNM n k t) = (vs ! n)^k * Iprod vs t"
+consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
+datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
+  | Or sgn sgn | And sgn sgn
+
+consts Isgn :: "('a::{ordered_idom, recpower}) list \<Rightarrow> sgn \<Rightarrow> bool"
+primrec 
+  "Isgn vs Tr = True"
+  "Isgn vs F = False"
+  "Isgn vs (ZeroEq t) = (Iprod vs t = 0)"
+  "Isgn vs (NZeroEq t) = (Iprod vs t \<noteq> 0)"
+  "Isgn vs (Pos t) = (Iprod vs t > 0)"
+  "Isgn vs (Neg t) = (Iprod vs t < 0)"
+  "Isgn vs (And p q) = (Isgn vs p \<and> Isgn vs q)"
+  "Isgn vs (Or p q) = (Isgn vs p \<or> Isgn vs q)"
+
+lemmas eqs = Isgn.simps Iprod.simps
+
+lemma "(x::int)^4 * y * z * y^2 * z^23 > 0"
+  apply (reify eqs)
+  oops
+
+
 end