# HG changeset patch
# User wenzelm
# Date 1087411049 -7200
# Node ID 0e94a1ccc6aeb7a24f3a6fbe06845bc6f38d9cd2
# Parent  70ec4b8aef8df0931ccdd6514cf8dc7920e68de0
tuned document;

diff -r 70ec4b8aef8d -r 0e94a1ccc6ae src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Wed Jun 16 20:37:14 2004 +0200
+++ b/src/FOL/ex/If.thy	Wed Jun 16 20:37:29 2004 +0200
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
+*)
 
-First-Order Logic: the 'if' example.
-*)
+header {* First-Order Logic: the 'if' example *}
 
 theory If = FOL:
 
@@ -49,16 +49,15 @@
 text{*An invalid formula.  High-level rules permit a simpler diagnosis*}
 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
 apply auto
-(*The next step will fail unless subgoals remain*)
+  -- {*The next step will fail unless subgoals remain*}
 apply (tactic all_tac)
 oops
 
 text{*Trying again from the beginning in order to prove from the definitions*}
 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
 apply (simp add: if_def, auto) 
-(*The next step will fail unless subgoals remain*)
+  -- {*The next step will fail unless subgoals remain*}
 apply (tactic all_tac)
 oops
 
-
 end
diff -r 70ec4b8aef8d -r 0e94a1ccc6ae src/FOL/ex/LocaleInst.thy
--- a/src/FOL/ex/LocaleInst.thy	Wed Jun 16 20:37:14 2004 +0200
+++ b/src/FOL/ex/LocaleInst.thy	Wed Jun 16 20:37:29 2004 +0200
@@ -12,7 +12,7 @@
 
 ML {* set show_hyps *}
 
-section {* Locale without assumptions *}
+subsection {* Locale without assumptions *}
 
 locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
 
@@ -32,7 +32,7 @@
   then show "A & B" ..
 qed
 
-section {* Simple locale with assumptions *}
+subsection {* Simple locale with assumptions *}
 
 typedecl i
 arities  i :: "term"
@@ -66,7 +66,7 @@
   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
 qed
 
-section {* Nested locale with assumptions *}
+subsection {* Nested locale with assumptions *}
 
 locale L3 =
   fixes OP (infixl "+" 60)
@@ -102,7 +102,7 @@
   show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
 qed
 
-section {* Locale with definition *}
+subsection {* Locale with definition *}
 
 text {* This example is admittedly not very creative :-) *}
 
@@ -119,7 +119,7 @@
   show ?thesis by (rule lem)  (* lem instantiated to True *)
 qed
 
-section {* Instantiation in a context with target *}
+subsection {* Instantiation in a context with target *}
 
 lemma (in L4)  (* Target might confuse instantiation command. *)
   fixes A (infixl "$" 60)
diff -r 70ec4b8aef8d -r 0e94a1ccc6ae src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Wed Jun 16 20:37:14 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Wed Jun 16 20:37:29 2004 +0200
@@ -168,7 +168,7 @@
 
 text {*
   For a set of natural numbers to be infinite, it is enough
-  to know that for any number larger than some $k$, there
+  to know that for any number larger than some @{text k}, there
   is some larger number that is an element of the set.
 *}
 
@@ -198,8 +198,8 @@
 
 text {*
   Every infinite set contains a countable subset. More precisely
-  we show that a set $S$ is infinite if and only if there exists 
-  an injective function from the naturals into $S$.
+  we show that a set @{text S} is infinite if and only if there exists 
+  an injective function from the naturals into @{text S}.
 *}
 
 lemma range_inj_infinite:
@@ -215,9 +215,9 @@
 text {*
   The ``only if'' direction is harder because it requires the
   construction of a sequence of pairwise different elements of
-  an infinite set $S$. The idea is to construct a sequence of
-  non-empty and infinite subsets of $S$ obtained by successively
-  removing elements of $S$.
+  an infinite set @{text S}. The idea is to construct a sequence of
+  non-empty and infinite subsets of @{text S} obtained by successively
+  removing elements of @{text S}.
 *}
 
 lemma linorder_injI: