adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
authorbulwahn
Wed May 18 15:45:33 2011 +0200 (2011-05-18)
changeset 428419079f49053e5
parent 42838 15727655bee2
child 42842 6ef538f6a8ab
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
src/HOL/IsaMakefile
src/HOL/Library/Code_Char_ord.thy
src/HOL/Library/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue May 17 22:29:55 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed May 18 15:45:33 2011 +0200
     1.3 @@ -437,7 +437,7 @@
     1.4    Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
     1.5    Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
     1.6    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
     1.7 -  Library/Code_Integer.thy Library/Code_Natural.thy			\
     1.8 +  Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy			\
     1.9    Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
    1.10    Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
    1.11    Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Code_Char_ord.thy	Wed May 18 15:45:33 2011 +0200
     2.3 @@ -0,0 +1,25 @@
     2.4 +(*  Title:      HOL/Library/Code_Char_ord.thy
     2.5 +    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
     2.6 +*)
     2.7 +
     2.8 +header {* Code generation of orderings for pretty characters *}
     2.9 +
    2.10 +theory Code_Char_ord
    2.11 +imports Code_Char Char_ord
    2.12 +begin
    2.13 +  
    2.14 +code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    2.15 +  (SML "!((_ : char) <= _)")
    2.16 +  (OCaml "<=")
    2.17 +  (Haskell infix 4 "<=")
    2.18 +  (Scala infixl 4 "<=")
    2.19 +  (Eval infixl 6 "<=")
    2.20 +
    2.21 +code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    2.22 +  (SML "!((_ : char) < _)")
    2.23 +  (OCaml "<")
    2.24 +  (Haskell infix 4 "<")
    2.25 +  (Scala infixl 4 "<")
    2.26 +  (Eval infixl 6 "<")
    2.27 +
    2.28 +end
    2.29 \ No newline at end of file
     3.1 --- a/src/HOL/Library/ROOT.ML	Tue May 17 22:29:55 2011 +0200
     3.2 +++ b/src/HOL/Library/ROOT.ML	Wed May 18 15:45:33 2011 +0200
     3.3 @@ -2,4 +2,4 @@
     3.4  (* Classical Higher-order Logic -- batteries included *)
     3.5  
     3.6  use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
     3.7 -  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
     3.8 +  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];