src/HOL/Presburger.thy
changeset 25230 022029099a83
parent 24993 92dfacb32053
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/Presburger.thy	Mon Oct 29 17:08:01 2007 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Tue Oct 30 08:45:54 2007 +0100
     1.3 @@ -703,6 +703,8 @@
     1.4    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
     1.5    less_number_of
     1.6  
     1.7 +context ring_1
     1.8 +begin
     1.9  
    1.10  lemma of_int_num [code func]:
    1.11    "of_int k = (if k = 0 then 0 else if k < 0 then
    1.12 @@ -737,3 +739,5 @@
    1.13  qed
    1.14  
    1.15  end
    1.16 +
    1.17 +end