summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 16 Jun 2004 20:37:29 +0200 | |

changeset 14957 | 0e94a1ccc6ae |

parent 14956 | 70ec4b8aef8d |

child 14958 | 801178863f17 |

tuned document;

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