Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Wed, 15 Jan 2014 08:01:36 +0100
changeset 55010 203b4f5482c3
parent 55009 d4b69107a86a
child 55011 e2042c4ae1b7
child 55012 e6cfa56a8bcd
tuned
src/HOL/IMP/Abs_Int1.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle