Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/RealOrd.thy
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 9043 ca761fe227d8
child 14265 95b42e69436c
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9013
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents: 8838
diff changeset 
     1
 
(*  Title:	 Real/RealOrd.thy
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents: 8838
diff changeset 
     2
 
    ID: 	 $Id$
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents: 8838
diff changeset 
     3
 
    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
7334
a90fc1e5fb19 Real/Real.thy main entry point;
wenzelm
parents:
diff changeset 
     4
 
    Copyright:   1998  University of Cambridge
9043
ca761fe227d8 First round of changes, towards installation of simprocs
paulson
parents: 9013
diff changeset 
     5
 
    Description: Type "real" is a linear order and also
ca761fe227d8 First round of changes, towards installation of simprocs
paulson
parents: 9013
diff changeset 
     6
 
                 satisfies plus_ac0: + is an AC-operator with zero
7334
a90fc1e5fb19 Real/Real.thy main entry point;
wenzelm
parents:
diff changeset 
     7
 
*)
a90fc1e5fb19 Real/Real.thy main entry point;
wenzelm
parents:
diff changeset 
     8
 












a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




     9


RealOrd = RealDef +













a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




    10














a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




    11


instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)













a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




    12


instance real :: linorder (real_le_linear)













a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




    13









9043






ca761fe227d8
First round of changes, towards installation of simprocs



paulson


parents: 
9013

diff
changeset




    14


instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)













ca761fe227d8
First round of changes, towards installation of simprocs



paulson


parents: 
9013

diff
changeset




    15









7334






a90fc1e5fb19
Real/Real.thy main entry point;



wenzelm


parents: 

diff
changeset




    16


end















isabelle