# HG changeset patch
# User haftmann
# Date 1204894381 -3600
# Node ID 075264a0a4bcadb641e7a8e991e2c9ffcdbd7919
# Parent  cd9d7f449369b899aded9e09afb9f35c608e5f33
canonical order on option type

diff -r cd9d7f449369 -r 075264a0a4bc src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 07 13:53:00 2008 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 07 13:53:01 2008 +0100
@@ -226,6 +226,7 @@
   Library/Library/ROOT.ML Library/Library/document/root.tex \
   Library/Library/document/root.bib Library/While_Combinator.thy \
   Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
+  Library/Option_ord.thy \
   Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
   Library/Coinductive_List.thy Library/AssocList.thy \
   Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
diff -r cd9d7f449369 -r 075264a0a4bc src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Mar 07 13:53:00 2008 +0100
+++ b/src/HOL/Library/Library.thy	Fri Mar 07 13:53:01 2008 +0100
@@ -32,6 +32,7 @@
   Nested_Environment
   Numeral_Type
   OptionalSugar
+  Option_ord
   Parity
   Permutation
   Primes