equal
deleted
inserted
replaced
144 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
144 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
145 fun afterqed [[totality]] lthy = |
145 fun afterqed [[totality]] lthy = |
146 let |
146 let |
147 val totality = Thm.close_derivation totality |
147 val totality = Thm.close_derivation totality |
148 val remove_domain_condition = |
148 val remove_domain_condition = |
149 full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
149 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
150 val tsimps = map remove_domain_condition psimps |
150 val tsimps = map remove_domain_condition psimps |
151 val tinduct = map remove_domain_condition pinducts |
151 val tinduct = map remove_domain_condition pinducts |
152 |
152 |
153 fun qualify n = Binding.name n |
153 fun qualify n = Binding.name n |
154 |> Binding.qualify true defname |
154 |> Binding.qualify true defname |