equal
deleted
inserted
replaced
84 val simpset = |
84 val simpset = |
85 Simplifier.global_context thy |
85 Simplifier.global_context thy |
86 (HOL_basic_ss addsimps |
86 (HOL_basic_ss addsimps |
87 (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))); |
87 (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))); |
88 fun prove prop = |
88 fun prove prop = |
89 Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset))) |
89 Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simpset))) |
90 |> Simpdata.mk_eq; |
90 |> Simpdata.mk_eq; |
91 in (map prove (triv_injects @ injects @ distincts), prove refl) end; |
91 in (map prove (triv_injects @ injects @ distincts), prove refl) end; |
92 |
92 |
93 fun add_equality vs tycos thy = |
93 fun add_equality vs tycos thy = |
94 let |
94 let |