# HG changeset patch
# User wenzelm
# Date 933609526 -7200
# Node ID 820c8c8573d9894d89e833175bfd9fb128b75a0c
# Parent  44d46a112127d3565f1817533a8dc6af9170077c
tuned;

diff -r 44d46a112127 -r 820c8c8573d9 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Mon Aug 02 17:58:46 1999 +0200
@@ -8,13 +8,31 @@
 
 theory KnasterTarski = Main:;
 
+text {*
+
+ According to the book ``Introduction to Lattices and Order'' (by
+ B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
+ fixpoint theorem is as follows (pages 93--94).  Note that we have
+ dualized their argument, and tuned the notation a little bit.
+
+ \paragraph{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
+ complete lattice and $f \colon L \to L$ an order-preserving map.
+ Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
+
+ \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
+ \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
+ \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
+ We now use this inequality to prove the reverse one (!) and thereby
+ complete the proof that $a$ is a fixpoint.  Since $f$ is
+ order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
+ \le f(a)$.
+*};
 
 text {*
- The proof of Knaster-Tarski below closely follows the presentation in
- 'Introduction to Lattices' and Order by Davey/Priestley, pages
- 93--94.  All of their narration has been rephrased in terms of formal
- Isar language elements.  Just as many textbook-style proofs, there is
- a strong bias towards forward reasoning, and little hierarchical
+ Our proof below closely follows this presentation.  Virtually all of
+ the prose narration has been rephrased in terms of formal Isar
+ language elements.  Just as many textbook-style proofs, there is a
+ strong bias towards forward reasoning, and little hierarchical
  structure.
 *};
 
diff -r 44d46a112127 -r 820c8c8573d9 src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Mon Aug 02 17:58:46 1999 +0200
@@ -17,7 +17,7 @@
     have ab: "A --> B";
     proof;
       assume a: A;
-      from not_a a; show B; ..;
+      show B; by contradiction;
     qed;
 
     from aba ab; show A; ..;
diff -r 44d46a112127 -r 820c8c8573d9 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Mon Aug 02 17:58:23 1999 +0200
+++ b/src/HOL/cladata.ML	Mon Aug 02 17:58:46 1999 +0200
@@ -76,7 +76,8 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
-  val cla_method' = Classical.cla_method'
+  val cla_modifiers = Classical.cla_modifiers;
+  val cla_meth' = Classical.cla_meth'
   end;
 
 structure Blast = BlastFun(Blast_Data);
diff -r 44d46a112127 -r 820c8c8573d9 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon Aug 02 17:58:23 1999 +0200
+++ b/src/Provers/clasimp.ML	Mon Aug 02 17:58:46 1999 +0200
@@ -149,7 +149,8 @@
 
 (* methods *)
 
-fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
+fun get_local_clasimpset ctxt =
+  (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
 
 val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
 val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
@@ -166,7 +167,7 @@
 
 val setup =
  [Method.add_methods
-   [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"),
+   [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp (improper!)"),
     ("auto", clasimp_method auto_tac, "auto"),
     ("force", clasimp_method' force_tac, "force"),
     ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]];