equal
deleted
inserted
replaced
222 interpretation option!: |
222 interpretation option!: |
223 partial_function_definitions "flat_ord None" "flat_lub None" |
223 partial_function_definitions "flat_ord None" "flat_lub None" |
224 by (rule flat_interpretation) |
224 by (rule flat_interpretation) |
225 |
225 |
226 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} |
226 declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} |
227 @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *} |
227 @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} |
228 |
228 |
229 declaration {* Partial_Function.init "option" @{term option.fixp_fun} |
229 declaration {* Partial_Function.init "option" @{term option.fixp_fun} |
230 @{term option.mono_body} @{thm option.fixp_rule_uc} *} |
230 @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *} |
231 |
231 |
232 |
232 |
233 abbreviation "option_ord \<equiv> flat_ord None" |
233 abbreviation "option_ord \<equiv> flat_ord None" |
234 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
234 abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" |
235 |
235 |