src/HOL/OrderedGroup.thy
changeset 29269 5c25a2012975
parent 28823 dcbef866c9e2
child 29557 5362cc5ee3a8
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:   HOL/OrderedGroup.thy
     1.5 -    ID:      $Id$
     1.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     1.7 -             with contributions by Jeremy Avigad
     1.8 +    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
     1.9  *)
    1.10  
    1.11  header {* Ordered Groups *}
    1.12 @@ -1376,7 +1374,7 @@
    1.13          @{const_name HOL.uminus}, @{const_name HOL.minus}]
    1.14    | agrp_ord _ = ~1;
    1.15  
    1.16 -fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    1.17 +fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
    1.18  
    1.19  local
    1.20    val ac1 = mk_meta_eq @{thm add_assoc};