equal
deleted
inserted
replaced
7 theory Partial_Function |
7 theory Partial_Function |
8 imports Complete_Partial_Order Fun_Def_Base Option |
8 imports Complete_Partial_Order Fun_Def_Base Option |
9 keywords "partial_function" :: thy_decl |
9 keywords "partial_function" :: thy_decl |
10 begin |
10 begin |
11 |
11 |
|
12 named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
12 ML_file "Tools/Function/partial_function.ML" |
13 ML_file "Tools/Function/partial_function.ML" |
13 setup Partial_Function.setup |
14 |
14 |
15 |
15 subsection {* Axiomatic setup *} |
16 subsection {* Axiomatic setup *} |
16 |
17 |
17 text {* This techical locale constains the requirements for function |
18 text {* This techical locale constains the requirements for function |
18 definitions with ccpo fixed points. *} |
19 definitions with ccpo fixed points. *} |