src/HOL/Library/Efficient_Nat.thy
changeset 48073 1b609a7837ef
parent 47108 2a1953f0d20d
child 48431 6efff142bb54
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 05 07:05:56 2012 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 05 07:10:51 2012 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4    (SML "!(raise/ Fail/ \"sub\")")
     1.5    (OCaml "failwith/ \"sub\"")
     1.6    (Haskell "error/ \"sub\"")
     1.7 -  (Scala "!error(\"sub\")")
     1.8 +  (Scala "!sys.error(\"sub\")")
     1.9  
    1.10  code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
    1.11    (SML "IntInf.*/ ((_),/ (_))")
    1.12 @@ -269,7 +269,7 @@
    1.13    (SML "!(raise/ Fail/ \"num'_of'_nat\")")
    1.14    (OCaml "failwith/ \"num'_of'_nat\"")
    1.15    (Haskell "error/ \"num'_of'_nat\"")
    1.16 -  (Scala "!error(\"num'_of'_nat\")")
    1.17 +  (Scala "!sys.error(\"num'_of'_nat\")")
    1.18  
    1.19  
    1.20  subsection {* Evaluation *}