author paulson Thu, 29 Mar 2007 11:59:54 +0200 changeset 22547 c3290f4382e4 parent 22546 c40d7ab8cbc5 child 22548 6ce4bddf3bcb
simplified some steps
 src/HOL/ex/Tarski.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/Tarski.thy	Thu Mar 29 11:12:39 2007 +0200
+++ b/src/HOL/ex/Tarski.thy	Thu Mar 29 11:59:54 2007 +0200
@@ -431,7 +431,7 @@
lemma (in CLF) monotone_f: "monotone f A r"

-lemma (in CLF) CLF_dual: "(cl,f) \<in> CLF ==> (dual cl, f) \<in> CLF"
+lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF"
apply (simp add: CLF_def  CL_dualCL monotone_dual)
done
@@ -536,7 +536,7 @@
apply (rule CLF.lubH_is_fixp)
apply (rule dualPO)
apply (rule CL_dualCL)
-apply (rule f_cl [THEN CLF_dual])
+apply (rule CLF_dual)
done

@@ -700,7 +700,7 @@
lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
apply (rule dualA_iff [THEN subst])
-apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual f_cl)
+apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
done

lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
@@ -731,8 +731,7 @@
prefer 2 apply assumption