equal
deleted
inserted
replaced
55 fun by_schematic_rule ctxt ct = |
55 fun by_schematic_rule ctxt ct = |
56 the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) |
56 the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) |
57 |
57 |
58 val z3_rules_setup = |
58 val z3_rules_setup = |
59 Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> |
59 Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> |
60 PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) |
60 Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) |
61 |
61 |
62 end |
62 end |
63 |
63 |
64 |
64 |
65 |
65 |