90 (* concrete syntax *) |
90 (* concrete syntax *) |
91 |
91 |
92 val trans_att = Attrib.add_del_args trans_add trans_del; |
92 val trans_att = Attrib.add_del_args trans_add trans_del; |
93 val sym_att = Attrib.add_del_args sym_add sym_del; |
93 val sym_att = Attrib.add_del_args sym_add sym_del; |
94 |
94 |
95 val _ = Context.>> |
95 val _ = Context.>> (Context.map_theory |
96 (Attrib.add_attributes |
96 (Attrib.add_attributes |
97 [("trans", trans_att, "declaration of transitivity rule"), |
97 [("trans", trans_att, "declaration of transitivity rule"), |
98 ("sym", sym_att, "declaration of symmetry rule"), |
98 ("sym", sym_att, "declaration of symmetry rule"), |
99 ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #> |
99 ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #> |
100 PureThy.add_thms |
100 PureThy.add_thms |
101 [(("", transitive_thm), [trans_add]), |
101 [(("", transitive_thm), [trans_add]), |
102 (("", symmetric_thm), [sym_add])] #> snd); |
102 (("", symmetric_thm), [sym_add])] #> snd)); |
103 |
103 |
104 |
104 |
105 |
105 |
106 (** proof commands **) |
106 (** proof commands **) |
107 |
107 |