| changeset 55010 | 203b4f5482c3 |
| parent 53015 | a1119cf551e8 |
| child 57512 | cc97b347b301 |
--- a/src/HOL/IMP/Abs_Int1.thy Tue Jan 14 18:41:24 2014 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Wed Jan 15 08:01:36 2014 +0100 @@ -100,7 +100,7 @@ subsubsection "Termination" locale Measure1 = -fixes m :: "'av::{order,order_top} \<Rightarrow> nat" +fixes m :: "'av::order_top \<Rightarrow> nat" fixes h :: "nat" assumes h: "m x \<le> h" begin