# HG changeset patch
# User bulwahn
# Date 1305726333 -7200
# Node ID 9079f49053e5ed7c7ffa059b8eb33c9a34859ef7
# Parent  15727655bee270777e9fdd431993b24d3950a565
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages

diff -r 15727655bee2 -r 9079f49053e5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 17 22:29:55 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed May 18 15:45:33 2011 +0200
@@ -437,7 +437,7 @@
   Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
   Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
-  Library/Code_Integer.thy Library/Code_Natural.thy			\
+  Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy			\
   Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
   Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
   Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
diff -r 15727655bee2 -r 9079f49053e5 src/HOL/Library/Code_Char_ord.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Char_ord.thy	Wed May 18 15:45:33 2011 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Library/Code_Char_ord.thy
+    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
+*)
+
+header {* Code generation of orderings for pretty characters *}
+
+theory Code_Char_ord
+imports Code_Char Char_ord
+begin
+  
+code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) <= _)")
+  (OCaml "<=")
+  (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
+
+code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) < _)")
+  (OCaml "<")
+  (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
+
+end
\ No newline at end of file
diff -r 15727655bee2 -r 9079f49053e5 src/HOL/Library/ROOT.ML
--- a/src/HOL/Library/ROOT.ML	Tue May 17 22:29:55 2011 +0200
+++ b/src/HOL/Library/ROOT.ML	Wed May 18 15:45:33 2011 +0200
@@ -2,4 +2,4 @@
 (* Classical Higher-order Logic -- batteries included *)
 
 use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
-  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
+  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];