src/HOL/Semiring_Normalization.thy
changeset 48891 c0eafbd55de3
parent 47108 2a1953f0d20d
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  theory Semiring_Normalization
     1.6  imports Numeral_Simprocs Nat_Transfer
     1.7 -uses
     1.8 -  "Tools/semiring_normalizer.ML"
     1.9  begin
    1.10  
    1.11 +ML_file "Tools/semiring_normalizer.ML"
    1.12 +
    1.13  text {* Prelude *}
    1.14  
    1.15  class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +