--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Nov 23 20:34:21 2006 +0100
@@ -5,6 +5,8 @@
chapter {* Aesthetics of ML programming *}
+text FIXME
+
text {* This style guide is loosely based on
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}.
% FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
@@ -85,7 +87,7 @@
while keeping its length to the absolutely neccessary minimum.
Always give the same name to function arguments which
have the same meaning. Separate words by underscores
- (``{\ttfamily int\_of\_string}'', not ``{\ttfamily intOfString}'')
+ (``@{verbatim int_of_string}'', not ``@{verbatim intOfString}'')
\end{description}
*}
--- a/src/HOL/Algebra/AbelCoset.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Thu Nov 23 20:34:21 2006 +0100
@@ -13,7 +13,7 @@
subsection {* Definitions *}
-text {* Hiding @{text "<+>"} from \texttt{Sum\_Type.thy} until I come
+text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
up with better syntax here *}
hide const Plus
--- a/src/HOL/Algebra/QuotRing.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Thu Nov 23 20:34:21 2006 +0100
@@ -114,7 +114,7 @@
--{* mult closed *}
apply (clarify)
apply (simp add: rcoset_mult_add, fast)
- --{* mult one\_closed *}
+ --{* mult @{text one_closed} *}
apply (force intro: one_closed)
--{* mult assoc *}
apply clarify
--- a/src/HOL/Algebra/RingHom.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/RingHom.thy Thu Nov 23 20:34:21 2006 +0100
@@ -11,7 +11,7 @@
section {* Homomorphisms of Non-Commutative Rings *}
-text {* Lifting existing lemmas in a ring\_hom\_ring locale *}
+text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
locale ring_hom_ring = ring R + ring S + var h +
assumes homh: "h \<in> ring_hom R S"
notes hom_mult [simp] = ring_hom_mult [OF homh]
--- a/src/HOL/Algebra/UnivPoly.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Nov 23 20:34:21 2006 +0100
@@ -1161,8 +1161,9 @@
text {* Further properties of the evaluation homomorphism. *}
-(* The following lemma could be proved in UP\_cring with the additional
- assumption that h is closed. *)
+text {*
+ The following lemma could be proved in @{text UP_cring} with the additional
+ assumption that @{text h} is closed. *}
lemma (in UP_pre_univ_prop) eval_const:
"[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
--- a/src/HOL/HOL.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/HOL.thy Thu Nov 23 20:34:21 2006 +0100
@@ -259,7 +259,7 @@
shows "A = B"
by (unfold meq) (rule refl)
-text {* Useful with eresolve\_tac for proving equalities from known equalities. *}
+text {* Useful with @{text erule} for proving equalities from known equalities. *}
(* a = b
| |
c = d *)
@@ -1403,7 +1403,7 @@
"f (if c then x else y) = (if c then f x else f y)"
by simp
-text {* For expand\_case\_tac *}
+text {* For @{text expand_case_tac} *}
lemma expand_case:
assumes "P \<Longrightarrow> Q True"
and "~P \<Longrightarrow> Q False"
@@ -1418,7 +1418,7 @@
qed
text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
- side of an equality. Used in {Integ,Real}/simproc.ML *}
+ side of an equality. Used in @{text "{Integ,Real}/simproc.ML"} *}
lemma restrict_to_left:
assumes "x = y"
shows "(x = z) = (y = z)"
--- a/src/HOL/SetInterval.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/SetInterval.thy Thu Nov 23 20:34:21 2006 +0100
@@ -627,7 +627,7 @@
the middle column shows the new (default) syntax, and the right column
shows a special syntax. The latter is only meaningful for latex output
and has to be activated explicitly by setting the print mode to
-\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in
+@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in
antiquotations). It is not the default \LaTeX\ output because it only
works well with italic-style formulae, not tt-style.
--- a/src/HOL/ex/Refute_Examples.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Thu Nov 23 20:34:21 2006 +0100
@@ -480,11 +480,11 @@
subsection {* Inductive datatypes *}
-text {* With quick\_and\_dirty set, the datatype package does not generate
- certain axioms for recursion operators. Without these axioms, refute may
- find spurious countermodels. *}
+text {* With @{text quick_and_dirty} set, the datatype package does
+ not generate certain axioms for recursion operators. Without these
+ axioms, refute may find spurious countermodels. *}
-ML {* reset quick_and_dirty; *}
+ML {* reset quick_and_dirty *}
subsubsection {* unit *}