44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
45 |> Pretty.chunks |> Pretty.writeln |
45 |> Pretty.chunks |> Pretty.writeln |
46 end; |
46 end; |
47 ); |
47 ); |
48 |
48 |
49 val _ = Context.add_setup [CalculationData.init]; |
49 val _ = Context.add_setup CalculationData.init; |
50 val print_rules = CalculationData.print; |
50 val print_rules = CalculationData.print; |
51 |
51 |
52 |
52 |
53 (* access calculation *) |
53 (* access calculation *) |
54 |
54 |
95 |
95 |
96 val trans_att = Attrib.add_del_args trans_add trans_del; |
96 val trans_att = Attrib.add_del_args trans_add trans_del; |
97 val sym_att = Attrib.add_del_args sym_add sym_del; |
97 val sym_att = Attrib.add_del_args sym_add sym_del; |
98 |
98 |
99 val _ = Context.add_setup |
99 val _ = Context.add_setup |
100 [Attrib.add_attributes |
100 (Attrib.add_attributes |
101 [("trans", Attrib.common trans_att, "declaration of transitivity rule"), |
101 [("trans", Attrib.common trans_att, "declaration of transitivity rule"), |
102 ("sym", Attrib.common sym_att, "declaration of symmetry rule"), |
102 ("sym", Attrib.common sym_att, "declaration of symmetry rule"), |
103 ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")], |
103 ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #> |
104 snd o PureThy.add_thms |
104 PureThy.add_thms |
105 [(("", transitive_thm), [Attrib.theory trans_add]), |
105 [(("", transitive_thm), [Attrib.theory trans_add]), |
106 (("", symmetric_thm), [Attrib.theory sym_add])]]; |
106 (("", symmetric_thm), [Attrib.theory sym_add])] #> snd); |
107 |
107 |
108 |
108 |
109 |
109 |
110 (** proof commands **) |
110 (** proof commands **) |
111 |
111 |