equal
deleted
inserted
replaced
63 datatype termlets = If | Case of (typ * int) |
63 datatype termlets = If | Case of (typ * int) |
64 |
64 |
65 fun simproc ss redex = |
65 fun simproc ss redex = |
66 let |
66 let |
67 val ctxt = Simplifier.the_context ss |
67 val ctxt = Simplifier.the_context ss |
68 val thy = ProofContext.theory_of ctxt |
68 val thy = Proof_Context.theory_of ctxt |
69 val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] |
69 val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] |
70 val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} |
70 val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} |
71 val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} |
71 val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} |
72 val del_refl_eq = @{lemma "(t = t & P) == P" by simp} |
72 val del_refl_eq = @{lemma "(t = t & P) == P" by simp} |
73 fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T) |
73 fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T) |