# HG changeset patch
# User wenzelm
# Date 1164310461 -3600
# Node ID 7f3ea2b3bab66706341786bc2ba53b734aa63afb
# Parent  8dab1e45c11f0447e0c7d76f5fcbbac0500270a5
prefer antiquotations over LaTeX macros;

diff -r 8dab1e45c11f -r 7f3ea2b3bab6 doc-src/IsarImplementation/Thy/ML.thy
--- 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}
 *}
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/Algebra/AbelCoset.thy
--- 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
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/Algebra/QuotRing.thy
--- 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
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/Algebra/RingHom.thy
--- 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]
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/Algebra/UnivPoly.thy
--- 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"
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/HOL.thy
--- 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)"
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/SetInterval.thy
--- 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.
 
diff -r 8dab1e45c11f -r 7f3ea2b3bab6 src/HOL/ex/Refute_Examples.thy
--- 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 *}