equal
deleted
inserted
replaced
122 burrow_fact (name_thms true official name) fact; |
122 burrow_fact (name_thms true official name) fact; |
123 |
123 |
124 |
124 |
125 (* enter_thms *) |
125 (* enter_thms *) |
126 |
126 |
127 fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy); |
127 fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy); |
128 |
128 |
129 fun enter_thms pre_name post_name app_att (b, thms) thy = |
129 fun enter_thms pre_name post_name app_att (b, thms) thy = |
130 if Binding.is_empty b |
130 if Binding.is_empty b |
131 then app_att thms thy |-> register_proofs |
131 then app_att thms thy |-> register_proofs |
132 else |
132 else |