prefer antiquotations over LaTeX macros;
authorwenzelm
Thu Nov 23 20:34:21 2006 +0100 (2006-11-23)
changeset 215027f3ea2b3bab6
parent 21501 8dab1e45c11f
child 21503 c4ea7e8c3937
prefer antiquotations over LaTeX macros;
doc-src/IsarImplementation/Thy/ML.thy
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/HOL.thy
src/HOL/SetInterval.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Nov 23 20:33:42 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Nov 23 20:34:21 2006 +0100
     1.3 @@ -5,6 +5,8 @@
     1.4  
     1.5  chapter {* Aesthetics of ML programming *}
     1.6  
     1.7 +text FIXME
     1.8 +
     1.9  text {* This style guide is loosely based on
    1.10    \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}.
    1.11  %  FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
    1.12 @@ -85,7 +87,7 @@
    1.13        while keeping its length to the absolutely neccessary minimum.
    1.14        Always give the same name to function arguments which
    1.15        have the same meaning. Separate words by underscores
    1.16 -      (``{\ttfamily int\_of\_string}'', not ``{\ttfamily intOfString}'')
    1.17 +      (``@{verbatim int_of_string}'', not ``@{verbatim intOfString}'')
    1.18  
    1.19    \end{description}
    1.20  *}
     2.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Nov 23 20:33:42 2006 +0100
     2.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Nov 23 20:34:21 2006 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  subsection {* Definitions *}
     2.6  
     2.7 -text {* Hiding @{text "<+>"} from \texttt{Sum\_Type.thy} until I come
     2.8 +text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
     2.9    up with better syntax here *}
    2.10  
    2.11  hide const Plus
     3.1 --- a/src/HOL/Algebra/QuotRing.thy	Thu Nov 23 20:33:42 2006 +0100
     3.2 +++ b/src/HOL/Algebra/QuotRing.thy	Thu Nov 23 20:34:21 2006 +0100
     3.3 @@ -114,7 +114,7 @@
     3.4        --{* mult closed *}
     3.5        apply (clarify)
     3.6        apply (simp add: rcoset_mult_add, fast)
     3.7 -     --{* mult one\_closed *}
     3.8 +     --{* mult @{text one_closed} *}
     3.9       apply (force intro: one_closed)
    3.10      --{* mult assoc *}
    3.11      apply clarify
     4.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Nov 23 20:33:42 2006 +0100
     4.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Nov 23 20:34:21 2006 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  section {* Homomorphisms of Non-Commutative Rings *}
     4.6  
     4.7 -text {* Lifting existing lemmas in a ring\_hom\_ring locale *}
     4.8 +text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
     4.9  locale ring_hom_ring = ring R + ring S + var h +
    4.10    assumes homh: "h \<in> ring_hom R S"
    4.11    notes hom_mult [simp] = ring_hom_mult [OF homh]
     5.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Nov 23 20:33:42 2006 +0100
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Nov 23 20:34:21 2006 +0100
     5.3 @@ -1161,8 +1161,9 @@
     5.4  
     5.5  text {* Further properties of the evaluation homomorphism. *}
     5.6  
     5.7 -(* The following lemma could be proved in UP\_cring with the additional
     5.8 -   assumption that h is closed. *)
     5.9 +text {*
    5.10 +  The following lemma could be proved in @{text UP_cring} with the additional
    5.11 +  assumption that @{text h} is closed. *}
    5.12  
    5.13  lemma (in UP_pre_univ_prop) eval_const:
    5.14    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
     6.1 --- a/src/HOL/HOL.thy	Thu Nov 23 20:33:42 2006 +0100
     6.2 +++ b/src/HOL/HOL.thy	Thu Nov 23 20:34:21 2006 +0100
     6.3 @@ -259,7 +259,7 @@
     6.4    shows "A = B"
     6.5    by (unfold meq) (rule refl)
     6.6  
     6.7 -text {* Useful with eresolve\_tac for proving equalities from known equalities. *}
     6.8 +text {* Useful with @{text erule} for proving equalities from known equalities. *}
     6.9       (* a = b
    6.10          |   |
    6.11          c = d   *)
    6.12 @@ -1403,7 +1403,7 @@
    6.13    "f (if c then x else y) = (if c then f x else f y)"
    6.14    by simp
    6.15  
    6.16 -text {* For expand\_case\_tac *}
    6.17 +text {* For @{text expand_case_tac} *}
    6.18  lemma expand_case:
    6.19    assumes "P \<Longrightarrow> Q True"
    6.20        and "~P \<Longrightarrow> Q False"
    6.21 @@ -1418,7 +1418,7 @@
    6.22  qed
    6.23  
    6.24  text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
    6.25 -  side of an equality.  Used in {Integ,Real}/simproc.ML *}
    6.26 +  side of an equality.  Used in @{text "{Integ,Real}/simproc.ML"} *}
    6.27  lemma restrict_to_left:
    6.28    assumes "x = y"
    6.29    shows "(x = z) = (y = z)"
     7.1 --- a/src/HOL/SetInterval.thy	Thu Nov 23 20:33:42 2006 +0100
     7.2 +++ b/src/HOL/SetInterval.thy	Thu Nov 23 20:34:21 2006 +0100
     7.3 @@ -627,7 +627,7 @@
     7.4  the middle column shows the new (default) syntax, and the right column
     7.5  shows a special syntax. The latter is only meaningful for latex output
     7.6  and has to be activated explicitly by setting the print mode to
     7.7 -\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in
     7.8 +@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in
     7.9  antiquotations). It is not the default \LaTeX\ output because it only
    7.10  works well with italic-style formulae, not tt-style.
    7.11  
     8.1 --- a/src/HOL/ex/Refute_Examples.thy	Thu Nov 23 20:33:42 2006 +0100
     8.2 +++ b/src/HOL/ex/Refute_Examples.thy	Thu Nov 23 20:34:21 2006 +0100
     8.3 @@ -480,11 +480,11 @@
     8.4  
     8.5  subsection {* Inductive datatypes *}
     8.6  
     8.7 -text {* With quick\_and\_dirty set, the datatype package does not generate
     8.8 -  certain axioms for recursion operators.  Without these axioms, refute may
     8.9 -  find spurious countermodels. *}
    8.10 +text {* With @{text quick_and_dirty} set, the datatype package does
    8.11 +  not generate certain axioms for recursion operators.  Without these
    8.12 +  axioms, refute may find spurious countermodels. *}
    8.13  
    8.14 -ML {* reset quick_and_dirty; *}
    8.15 +ML {* reset quick_and_dirty *}
    8.16  
    8.17  subsubsection {* unit *}
    8.18