author wenzelm Wed, 16 Jun 2004 20:37:29 +0200 changeset 14957 0e94a1ccc6ae parent 14956 70ec4b8aef8d child 14958 801178863f17
tuned document;
 src/FOL/ex/If.thy file | annotate | diff | comparison | revisions src/FOL/ex/LocaleInst.thy file | annotate | diff | comparison | revisions src/HOL/Infinite_Set.thy file | annotate | diff | comparison | revisions
```--- 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
+*)

-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))"
-(*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:```