equal
deleted
inserted
replaced
84 (Haskell infixl 4 "==") |
84 (Haskell infixl 4 "==") |
85 |
85 |
86 |
86 |
87 text {* type bool *} |
87 text {* type bool *} |
88 |
88 |
89 lemmas [code func, code unfold] = imp_conv_disj |
89 lemmas [code func, code unfold, code post] = imp_conv_disj |
90 |
90 |
91 code_type bool |
91 code_type bool |
92 (SML "bool") |
92 (SML "bool") |
93 (OCaml "bool") |
93 (OCaml "bool") |
94 (Haskell "Bool") |
94 (Haskell "Bool") |
145 |
145 |
146 subsection {* Normalization by evaluation *} |
146 subsection {* Normalization by evaluation *} |
147 |
147 |
148 method_setup normalization = {* |
148 method_setup normalization = {* |
149 Method.no_args (Method.SIMPLE_METHOD' |
149 Method.no_args (Method.SIMPLE_METHOD' |
150 (fn k => CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) k |
150 (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) |
151 THEN TRYALL (resolve_tac [TrueI]) |
151 THEN' (fn k => TRY (rtac TrueI k)) |
152 )) |
152 )) |
153 *} "solve goal by normalization" |
153 *} "solve goal by normalization" |
154 |
154 |
155 end |
155 end |