equal
deleted
inserted
replaced
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 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 "Tools/Function/partial_function.ML" |
13 ML_file \<open>Tools/Function/partial_function.ML\<close> |
14 |
14 |
15 lemma (in ccpo) in_chain_finite: |
15 lemma (in ccpo) in_chain_finite: |
16 assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}" |
16 assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}" |
17 shows "\<Squnion>A \<in> A" |
17 shows "\<Squnion>A \<in> A" |
18 using assms(2,1,3) |
18 using assms(2,1,3) |