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.
canonical order on option type
authorhaftmann
Fri, 07 Mar 2008 13:53:01 +0100
changeset 26232 075264a0a4bc
parent 26231 cd9d7f449369
child 26233 3751b3dbb67c
canonical order on option type
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Library/Library.thy file | annotate | diff | comparison | revisions 
--- 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 \
--- 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
isabelle