src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
changeset 58678 398e05aa84d4
parent 54228 229282d53781
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Tue Oct 14 16:19:42 2014 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -16,20 +16,6 @@
     1.4    by a corresponding @{text export_code} command.
     1.5  *}
     1.6  
     1.7 -text {* Formal joining of hierarchy of implicit definitions in Scala *}
     1.8 -
     1.9 -class semiring_numeral_even_odd = semiring_numeral_div + even_odd
    1.10 -
    1.11 -instance nat :: semiring_numeral_even_odd ..
    1.12 -
    1.13 -definition semiring_numeral_even_odd :: "'a itself \<Rightarrow> 'a::semiring_numeral_even_odd"
    1.14 -where
    1.15 -  "semiring_numeral_even_odd TYPE('a) = undefined"
    1.16 -
    1.17 -definition semiring_numeral_even_odd_nat :: "nat itself \<Rightarrow> nat"
    1.18 -where
    1.19 -  "semiring_numeral_even_odd_nat = semiring_numeral_even_odd"
    1.20 -
    1.21 -export_code _ checking  SML OCaml? Haskell? Scala
    1.22 +export_code _ checking SML OCaml? Haskell? Scala
    1.23  
    1.24  end