# HG changeset patch
# User huffman
# Date 1319467644 -7200
# Node ID b0cea4362430da9aaceb3397a3bfe6c7545d52cd
# Parent  8716790fe5a30847d7356cc50ee8c7076f4fae2f
instance bool :: linorder

diff -r 8716790fe5a3 -r b0cea4362430 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Oct 24 12:26:05 2011 +0200
+++ b/src/HOL/Orderings.thy	Mon Oct 24 16:47:24 2011 +0200
@@ -1232,7 +1232,7 @@
 
 subsection {* Order on bool *}
 
-instantiation bool :: "{bot, top}"
+instantiation bool :: "{bot, top, linorder}"
 begin
 
 definition