equal
deleted
inserted
replaced
150 *} "solve goal by evaluation" |
150 *} "solve goal by evaluation" |
151 |
151 |
152 |
152 |
153 subsection {* Normalization by evaluation *} |
153 subsection {* Normalization by evaluation *} |
154 |
154 |
155 setup Nbe.setup |
|
156 |
|
157 method_setup normalization = {* |
155 method_setup normalization = {* |
158 Method.no_args (Method.SIMPLE_METHOD' |
156 Method.no_args (Method.SIMPLE_METHOD' |
159 (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv) |
157 (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv) |
160 THEN' resolve_tac [TrueI, refl])) |
158 THEN' resolve_tac [TrueI, refl])) |
161 *} "solve goal by normalization" |
159 *} "solve goal by normalization" |