equal
deleted
inserted
replaced
5 header {* Partial Function Definitions *} |
5 header {* Partial Function Definitions *} |
6 |
6 |
7 theory Partial_Function |
7 theory Partial_Function |
8 imports Complete_Partial_Order Option |
8 imports Complete_Partial_Order Option |
9 keywords "partial_function" :: thy_decl |
9 keywords "partial_function" :: thy_decl |
10 uses |
|
11 "Tools/Function/function_lib.ML" |
|
12 "Tools/Function/partial_function.ML" |
|
13 begin |
10 begin |
14 |
11 |
|
12 ML_file "Tools/Function/function_lib.ML" |
|
13 ML_file "Tools/Function/partial_function.ML" |
15 setup Partial_Function.setup |
14 setup Partial_Function.setup |
16 |
15 |
17 subsection {* Axiomatic setup *} |
16 subsection {* Axiomatic setup *} |
18 |
17 |
19 text {* This techical locale constains the requirements for function |
18 text {* This techical locale constains the requirements for function |