src/HOL/List.thy
changeset 52435 6646bb548c6b
parent 52380 3cc46b8cca5e
child 53012 cb82606b8215
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/List.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -6042,30 +6042,31 @@
     1.4              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
     1.5          | NONE =>
     1.6              default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
     1.7 -  in Code_Target.add_const_syntax target @{const_name Cons}
     1.8 -    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
     1.9 +  in
    1.10 +    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
    1.11 +      [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
    1.12    end
    1.13  
    1.14  end;
    1.15  *}
    1.16  
    1.17 -code_type list
    1.18 -  (SML "_ list")
    1.19 -  (OCaml "_ list")
    1.20 -  (Haskell "![(_)]")
    1.21 -  (Scala "List[(_)]")
    1.22 -
    1.23 -code_const Nil
    1.24 -  (SML "[]")
    1.25 -  (OCaml "[]")
    1.26 -  (Haskell "[]")
    1.27 -  (Scala "!Nil")
    1.28 -
    1.29 -code_instance list :: equal
    1.30 -  (Haskell -)
    1.31 -
    1.32 -code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.33 -  (Haskell infix 4 "==")
    1.34 +code_printing
    1.35 +  type_constructor list \<rightharpoonup>
    1.36 +    (SML) "_ list"
    1.37 +    and (OCaml) "_ list"
    1.38 +    and (Haskell) "![(_)]"
    1.39 +    and (Scala) "List[(_)]"
    1.40 +| constant Nil \<rightharpoonup>
    1.41 +    (SML) "[]"
    1.42 +    and (OCaml) "[]"
    1.43 +    and (Haskell) "[]"
    1.44 +    and (Scala) "!Nil"
    1.45 +| class_instance list :: equal \<rightharpoonup>
    1.46 +    (Haskell) -
    1.47 +| constant "HOL.equal :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" \<rightharpoonup>
    1.48 +    (Haskell) infix 4 "=="
    1.49 +
    1.50 +setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
    1.51  
    1.52  code_reserved SML
    1.53    list
    1.54 @@ -6073,49 +6074,37 @@
    1.55  code_reserved OCaml
    1.56    list
    1.57  
    1.58 -setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
    1.59 -
    1.60  
    1.61  subsubsection {* Use convenient predefined operations *}
    1.62  
    1.63 -code_const "op @"
    1.64 -  (SML infixr 7 "@")
    1.65 -  (OCaml infixr 6 "@")
    1.66 -  (Haskell infixr 5 "++")
    1.67 -  (Scala infixl 7 "++")
    1.68 -
    1.69 -code_const map
    1.70 -  (Haskell "map")
    1.71 -
    1.72 -code_const filter
    1.73 -  (Haskell "filter")
    1.74 -
    1.75 -code_const concat
    1.76 -  (Haskell "concat")
    1.77 -
    1.78 -code_const List.maps
    1.79 -  (Haskell "concatMap")
    1.80 -
    1.81 -code_const rev
    1.82 -  (Haskell "reverse")
    1.83 -
    1.84 -code_const zip
    1.85 -  (Haskell "zip")
    1.86 -
    1.87 -code_const List.null
    1.88 -  (Haskell "null")
    1.89 -
    1.90 -code_const takeWhile
    1.91 -  (Haskell "takeWhile")
    1.92 -
    1.93 -code_const dropWhile
    1.94 -  (Haskell "dropWhile")
    1.95 -
    1.96 -code_const list_all
    1.97 -  (Haskell "all")
    1.98 -
    1.99 -code_const list_ex
   1.100 -  (Haskell "any")
   1.101 +code_printing
   1.102 +  constant "op @" \<rightharpoonup>
   1.103 +    (SML) infixr 7 "@"
   1.104 +    and (OCaml) infixr 6 "@"
   1.105 +    and (Haskell) infixr 5 "++"
   1.106 +    and (Scala) infixl 7 "++"
   1.107 +| constant map \<rightharpoonup>
   1.108 +    (Haskell) "map"
   1.109 +| constant filter \<rightharpoonup>
   1.110 +    (Haskell) "filter"
   1.111 +| constant concat \<rightharpoonup>
   1.112 +    (Haskell) "concat"
   1.113 +| constant List.maps \<rightharpoonup>
   1.114 +    (Haskell) "concatMap"
   1.115 +| constant rev \<rightharpoonup>
   1.116 +    (Haskell) "reverse"
   1.117 +| constant zip \<rightharpoonup>
   1.118 +    (Haskell) "zip"
   1.119 +| constant List.null \<rightharpoonup>
   1.120 +    (Haskell) "null"
   1.121 +| constant takeWhile \<rightharpoonup>
   1.122 +    (Haskell) "takeWhile"
   1.123 +| constant dropWhile \<rightharpoonup>
   1.124 +    (Haskell) "dropWhile"
   1.125 +| constant list_all \<rightharpoonup>
   1.126 +    (Haskell) "all"
   1.127 +| constant list_ex \<rightharpoonup>
   1.128 +    (Haskell) "any"
   1.129  
   1.130  
   1.131  subsubsection {* Implementation of sets by lists *}