# HG changeset patch
# User paulson
# Date 1175162394 -7200
# Node ID c3290f4382e4a4eaee0f943041e050e32b7686fc
# Parent  c40d7ab8cbc5c6c9876c57e4846b33c0b08b8143
simplified some steps

diff -r c40d7ab8cbc5 -r c3290f4382e4 src/HOL/ex/Tarski.thy
--- 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"
 by (simp add: A_def r_def)
 
-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)
 apply (simp add: dualA_iff)
 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)
 apply (simp add: dualr_iff dualA_iff)
 done
 
@@ -700,7 +700,7 @@
 lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
 apply (simp add: Top_dual_Bot A_def)
 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
 apply (simp add: A_def)
 apply (rule dualA_iff [THEN subst])
-apply (blast intro!: CLF.Top_in_lattice
-                 f_cl dualPO CL_dualCL CLF_dual)
+apply (blast intro!: CLF.Top_in_lattice dualPO CL_dualCL CLF_dual)
 apply (simp add: CLF.Top_intv_not_empty [of _ f]
                  dualA_iff A_def dualPO CL_dualCL CLF_dual)
 done