--- 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
--- 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)
--- 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: