| changeset 16417 | 9bc16273c2d4 |
| parent 15613 | ab90e95ae02e |
| child 18372 | 2bffdf62fe7f |
--- a/src/HOL/MicroJava/BV/Product.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/MicroJava/BV/Product.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ header {* \isaheader{Products as Semilattices} *} -theory Product = Err: +theory Product imports Err begin constdefs le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"