declare transitive;
authorwenzelm
Fri Nov 02 22:02:41 2001 +0100 (2001-11-02)
changeset 120218809efda06d3
parent 12020 a24373086908
child 12022 9c3377b133c0
declare transitive;
src/Pure/Isar/calculation.ML
     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;