1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Aug 30 15:18:09 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Tue Aug 31 10:19:02 2010 +0200
     1.3 @@ -59,8 +59,7 @@
     1.4  (*use_thy "Knowledge/Typefix" FIXXXMEWN100827*)
     1.5  use_thy "Knowledge/Descript"
     1.6  
     1.7 -ML {* @{thm sym} *}
     1.8 -ML {* @{thm } RS @{thm } *}
     1.9 +ML {* @{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)} *}
    1.10  
    1.11  ML {*"--------------------------------------------"*}
    1.12