equal
deleted
inserted
replaced
96 "declaration of transitivity rule" #> |
96 "declaration of transitivity rule" #> |
97 Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del) |
97 Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del) |
98 "declaration of symmetry rule" #> |
98 "declaration of symmetry rule" #> |
99 Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric) |
99 Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric) |
100 "resolution with symmetry rule" #> |
100 "resolution with symmetry rule" #> |
101 PureThy.add_thms |
101 Global_Theory.add_thms |
102 [((Binding.empty, transitive_thm), [trans_add]), |
102 [((Binding.empty, transitive_thm), [trans_add]), |
103 ((Binding.empty, symmetric_thm), [sym_add])] #> snd)); |
103 ((Binding.empty, symmetric_thm), [sym_add])] #> snd)); |
104 |
104 |
105 |
105 |
106 |
106 |