equal
deleted
inserted
replaced
69 val LK_basic_ss = |
69 val LK_basic_ss = |
70 empty_simpset @{context} |
70 empty_simpset @{context} |
71 setSSolver (mk_solver "safe" safe_solver) |
71 setSSolver (mk_solver "safe" safe_solver) |
72 setSolver (mk_solver "unsafe" unsafe_solver) |
72 setSolver (mk_solver "unsafe" unsafe_solver) |
73 |> Simplifier.set_subgoaler asm_simp_tac |
73 |> Simplifier.set_subgoaler asm_simp_tac |
74 |> Simplifier.set_mksimps (fn ctxt => |
74 |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) |
75 map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt)) |
|
76 |> Simplifier.set_mkcong mk_meta_cong |
75 |> Simplifier.set_mkcong mk_meta_cong |
77 |> simpset_of; |
76 |> simpset_of; |
78 |
77 |
79 val LK_simps = |
78 val LK_simps = |
80 [@{thm triv_forall_equality}, (* prunes params *) |
79 [@{thm triv_forall_equality}, (* prunes params *) |