equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>Partial Function Definitions\<close> |
5 section \<open>Partial Function Definitions\<close> |
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_defn |
10 begin |
10 begin |
11 |
11 |
12 named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
12 named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
13 ML_file \<open>Tools/Function/partial_function.ML\<close> |
13 ML_file \<open>Tools/Function/partial_function.ML\<close> |
14 |
14 |