equal
deleted
inserted
replaced
103 (DEPTH_SOLVE (etac @{thm FalseE} 1 |
103 (DEPTH_SOLVE (etac @{thm FalseE} 1 |
104 ORELSE basic_res_tac 1 |
104 ORELSE basic_res_tac 1 |
105 ORELSE (ares_tac hyps 1 |
105 ORELSE (ares_tac hyps 1 |
106 APPEND typecheck_step_tac (tcset_of ctxt)))); |
106 APPEND typecheck_step_tac (tcset_of ctxt)))); |
107 |
107 |
108 val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => |
108 val type_solver = |
109 type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
109 Simplifier.mk_solver "ZF typecheck" (fn ss => |
|
110 type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss)); |
110 |
111 |
111 |
112 |
112 (* concrete syntax *) |
113 (* concrete syntax *) |
113 |
114 |
114 val typecheck_setup = |
115 val typecheck_setup = |