1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Jul 15 08:28:50 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Wed Jul 17 07:32:53 2013 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4    ("List.if_True", (prop_of o num_str) @{thm if_True}),
     1.5    ("HOL.if_False", (prop_of o num_str) @{thm if_False}),
     1.6    (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)
     1.7 -  ("Rings.semiring_class.left_distrib", (prop_of o num_str) @{thm left_distrib}),
     1.8 -  ("Rings.semiring_class.right_distrib", (prop_of o num_str) @{thm right_distrib}),
     1.9 +  ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),
    1.10 +  ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),
    1.11    (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)
    1.12    (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)
    1.13    ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),