src/HOL/Library/Efficient_Nat.thy
changeset 28683 59c01ec6cb8d
parent 28562 4e74209f113e
child 28694 4e9edaef64dc
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 24 17:48:34 2008 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 24 17:48:35 2008 +0200
     1.3 @@ -445,16 +445,19 @@
     1.4  code_modulename SML
     1.5    Nat Integer
     1.6    Divides Integer
     1.7 +  Ring_and_Field Integer
     1.8    Efficient_Nat Integer
     1.9  
    1.10  code_modulename OCaml
    1.11    Nat Integer
    1.12    Divides Integer
    1.13 +  Ring_and_Field Integer
    1.14    Efficient_Nat Integer
    1.15  
    1.16  code_modulename Haskell
    1.17    Nat Integer
    1.18    Divides Integer
    1.19 +  Ring_and_Field Integer
    1.20    Efficient_Nat Integer
    1.21  
    1.22  hide const int