# HG changeset patch
# User nipkow
# Date 1365321997 -7200
# Node ID f0b375b692927b4ef06b2396c78d217ef62b64b1
# Parent  0a6d576da2959695a4051520d6820c52e7fdc979
cleaned

diff -r 0a6d576da295 -r f0b375b69292 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sat Apr 06 18:42:55 2013 +0200
+++ b/src/HOL/IMP/Collecting.thy	Sun Apr 07 10:06:37 2013 +0200
@@ -37,11 +37,6 @@
 
 subsubsection "Annotated commands as a complete lattice"
 
-(* Orderings could also be lifted generically (thus subsuming the
-instantiation for preord and order), but then less_eq_acom would need to
-become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
-need to unfold this defn first. *)
-
 instantiation acom :: (order) order
 begin