updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
header {* Prefixpoints *}
theory Ex4
imports LCF
begin
lemma example:
assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q"
shows "FIX(f)=p"
apply (unfold eq_def)
apply (rule conjI)
apply (tactic {* induct_tac @{context} "f" 1 *})
apply (rule minimal)
apply (intro strip)
apply (rule less_trans)
prefer 2
apply (rule asms)
apply (erule less_ap_term)
apply (rule asms)
apply (rule FIX_eq [THEN eq_imp_less1])
done
end