| changeset 32960 | 69916a850301 |
| parent 31021 | 53642251a04f |
| child 35028 | 108662d50512 |
--- a/src/HOL/ex/ReflectionEx.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/ex/ReflectionEx.thy Sat Oct 17 14:43:18 2009 +0200 @@ -382,7 +382,7 @@ oops - (* An example for equations containing type variables *) +(* 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 :: " prod \<Rightarrow> ('a::{ordered_idom}) list \<Rightarrow>'a"