src/Pure/Isar/calculation.ML
changeset 12021 8809efda06d3
parent 11784 b66b198ee29a
child 12055 a9c44895cc8c
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Nov 02 22:01:58 2001 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Nov 02 22:02:41 2001 +0100
     1.3 @@ -174,7 +174,8 @@
     1.4  (** theory setup **)
     1.5  
     1.6  val setup = [GlobalCalculation.init, LocalCalculation.init,
     1.7 -  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")]];
     1.8 +  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")],
     1.9 +  #1 o PureThy.add_thms [(("", transitive_thm), [trans_add_global])]];
    1.10  
    1.11  
    1.12  end;