prevent line breaks after Scala symbolic operators
authorhaftmann
Thu, 26 Aug 2010 12:19:49 +0200
changeset 39006f9837065b5e8
parent 39005 eb7bc47f062b
child 39007 567b94f8bb6e
prevent line breaks after Scala symbolic operators
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Code_Integer.thy
src/HOL/ex/Numeral.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 26 10:23:25 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Aug 26 12:19:49 2010 +0200
     1.3 @@ -1924,7 +1924,7 @@
     1.4    (Haskell "True" and "False" and "not"
     1.5      and infixl 3 "&&" and infixl 2 "||"
     1.6      and "!(if (_)/ then (_)/ else (_))")
     1.7 -  (Scala "true" and "false" and "'!/ _"
     1.8 +  (Scala "true" and "false" and "'! _"
     1.9      and infixl 3 "&&" and infixl 1 "||"
    1.10      and "!(if ((_))/ (_)/ else (_))")
    1.11  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 10:23:25 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 12:19:49 2010 +0200
     2.3 @@ -478,6 +478,7 @@
     2.4  
     2.5  code_include Scala "Heap"
     2.6  {*import collection.mutable.ArraySeq
     2.7 +
     2.8  def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
     2.9  
    2.10  class Ref[A](x: A) {
     3.1 --- a/src/HOL/Library/Code_Integer.thy	Thu Aug 26 10:23:25 2010 +0200
     3.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Aug 26 12:19:49 2010 +0200
     3.3 @@ -51,14 +51,14 @@
     3.4    (SML "IntInf.- ((_), 1)")
     3.5    (OCaml "Big'_int.pred'_big'_int")
     3.6    (Haskell "!(_/ -/ 1)")
     3.7 -  (Scala "!(_/ -/ 1)")
     3.8 +  (Scala "!(_ -/ 1)")
     3.9    (Eval "!(_/ -/ 1)")
    3.10  
    3.11  code_const Int.succ
    3.12    (SML "IntInf.+ ((_), 1)")
    3.13    (OCaml "Big'_int.succ'_big'_int")
    3.14    (Haskell "!(_/ +/ 1)")
    3.15 -  (Scala "!(_/ +/ 1)")
    3.16 +  (Scala "!(_ +/ 1)")
    3.17    (Eval "!(_/ +/ 1)")
    3.18  
    3.19  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
     4.1 --- a/src/HOL/ex/Numeral.thy	Thu Aug 26 10:23:25 2010 +0200
     4.2 +++ b/src/HOL/ex/Numeral.thy	Thu Aug 26 12:19:49 2010 +0200
     4.3 @@ -1033,14 +1033,14 @@
     4.4    (SML "IntInf.- ((_), 1)")
     4.5    (OCaml "Big'_int.pred'_big'_int")
     4.6    (Haskell "!(_/ -/ 1)")
     4.7 -  (Scala "!(_/ -/ 1)")
     4.8 +  (Scala "!(_ -/ 1)")
     4.9    (Eval "!(_/ -/ 1)")
    4.10  
    4.11  code_const Int.succ
    4.12    (SML "IntInf.+ ((_), 1)")
    4.13    (OCaml "Big'_int.succ'_big'_int")
    4.14    (Haskell "!(_/ +/ 1)")
    4.15 -  (Scala "!(_/ +/ 1)")
    4.16 +  (Scala "!(_ +/ 1)")
    4.17    (Eval "!(_/ +/ 1)")
    4.18  
    4.19  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"