equal
deleted
inserted
replaced
38 |
38 |
39 (* ------------------------------------------------------------------------ *) |
39 (* ------------------------------------------------------------------------ *) |
40 (* chains of functions yield chains in the po range *) |
40 (* chains of functions yield chains in the po range *) |
41 (* ------------------------------------------------------------------------ *) |
41 (* ------------------------------------------------------------------------ *) |
42 |
42 |
43 Goalw [chain] "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"; |
43 Goalw [chain_def] "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)"; |
44 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
44 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
45 qed "ch2ch_fun"; |
45 qed "ch2ch_fun"; |
46 |
46 |
47 (* ------------------------------------------------------------------------ *) |
47 (* ------------------------------------------------------------------------ *) |
48 (* upper bounds of function chains yield upper bound in the po range *) |
48 (* upper bounds of function chains yield upper bound in the po range *) |