equal
deleted
inserted
replaced
107 type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
107 type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); |
108 |
108 |
109 |
109 |
110 (* concrete syntax *) |
110 (* concrete syntax *) |
111 |
111 |
112 val typecheck_meth = |
112 val typecheck_setup = |
113 Method.sections |
113 Method.setup @{binding typecheck} |
114 [Args.add -- Args.colon >> K (I, TC_add), |
114 (Method.sections |
115 Args.del -- Args.colon >> K (I, TC_del)] |
115 [Args.add -- Args.colon >> K (I, TC_add), |
116 >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))); |
116 Args.del -- Args.colon >> K (I, TC_del)] |
|
117 >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))) |
|
118 "ZF type-checking"; |
117 |
119 |
118 val _ = |
120 val _ = |
119 OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
121 OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag |
120 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
122 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
121 Toplevel.keep (print_tcset o Toplevel.context_of))); |
123 Toplevel.keep (print_tcset o Toplevel.context_of))); |
123 |
125 |
124 (* theory setup *) |
126 (* theory setup *) |
125 |
127 |
126 val setup = |
128 val setup = |
127 Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #> |
129 Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #> |
128 Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #> |
130 typecheck_setup #> |
129 Simplifier.map_simpset (fn ss => ss setSolver type_solver); |
131 Simplifier.map_simpset (fn ss => ss setSolver type_solver); |
130 |
132 |
131 end; |
133 end; |