# HG changeset patch
# User wenzelm
# Date 1229451895 -3600
# Node ID 2a684ee023e750fa7feb60c11d3446926ee7669c
# Parent  970d746274d5953d463aa31920cf01d35a1707e7
proper document antiquotations;

diff -r 970d746274d5 -r 2a684ee023e7 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Tue Dec 16 18:04:31 2008 +0100
+++ b/src/HOL/FunDef.thy	Tue Dec 16 19:24:55 2008 +0100
@@ -235,7 +235,7 @@
 lemma wf_pair_less[simp]: "wf pair_less"
   by (auto simp: pair_less_def)
 
-text {* Introduction rules for pair_less/pair_leq *}
+text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"