diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Semiring_Normalization.thy --- a/src/HOL/Semiring_Normalization.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Semiring_Normalization.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,10 +6,10 @@ theory Semiring_Normalization imports Numeral_Simprocs Nat_Transfer -uses - "Tools/semiring_normalizer.ML" begin +ML_file "Tools/semiring_normalizer.ML" + text {* Prelude *} class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +