| changeset 57959 | 1bfed12a7646 |
| parent 55085 | 0e8e4dc55866 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Partial_Function.thy Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Partial_Function.thy Sat Aug 16 19:20:11 2014 +0200 @@ -9,8 +9,9 @@ keywords "partial_function" :: thy_decl begin +named_theorems partial_function_mono "monotonicity rules for partial function definitions" ML_file "Tools/Function/partial_function.ML" -setup Partial_Function.setup + subsection {* Axiomatic setup *}