| changeset 27680 | 5a557a5afc48 |
| parent 22271 | 51a80e238b29 |
| child 30235 | 58d147683393 |
--- a/src/HOL/MicroJava/BV/Opt.thy Fri Jul 25 12:03:28 2008 +0200 +++ b/src/HOL/MicroJava/BV/Opt.thy Fri Jul 25 12:03:31 2008 +0200 @@ -8,7 +8,9 @@ header {* \isaheader{More about Options} *} -theory Opt imports Err begin +theory Opt +imports Err +begin constdefs le :: "'a ord \<Rightarrow> 'a option ord"