equal
deleted
inserted
replaced
47 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
47 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
48 fun afterqed [[totality]] lthy = |
48 fun afterqed [[totality]] lthy = |
49 let |
49 let |
50 val totality = Thm.close_derivation totality |
50 val totality = Thm.close_derivation totality |
51 val remove_domain_condition = |
51 val remove_domain_condition = |
52 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
52 full_simplify (put_simpset HOL_basic_ss lthy |
|
53 addsimps [totality, @{thm True_implies_equals}]) |
53 val tsimps = map remove_domain_condition psimps |
54 val tsimps = map remove_domain_condition psimps |
54 val tinducts = map remove_domain_condition pinducts |
55 val tinducts = map remove_domain_condition pinducts |
55 val teqvts = map remove_domain_condition eqvts |
56 val teqvts = map remove_domain_condition eqvts |
56 |
57 |
57 fun qualify n = Binding.name n |
58 fun qualify n = Binding.name n |