# HG changeset patch # User nipkow # Date 1389769296 -3600 # Node ID 203b4f5482c32e9c43976e34860c88b281f2c64e # Parent d4b69107a86ae1964529efb2b70ae01e7c052ce2 tuned diff -r d4b69107a86a -r 203b4f5482c3 src/HOL/IMP/Abs_Int1.thy --- 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} \ nat" +fixes m :: "'av::order_top \ nat" fixes h :: "nat" assumes h: "m x \ h" begin