doc-src/TutorialI/Rules/Basic.thy

--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Aug 03 18:04:55 2001 +0200
@@ -277,6 +277,9 @@
 Hilbert-epsilon theorems*}
 
 text{*
+@{thm[display] the_equality[no_vars]}
+\rulename{the_equality}
+
 @{thm[display] some_equality[no_vars]}
 \rulename{some_equality}
 
@@ -311,7 +314,7 @@
      "\<lbrakk> P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
 apply (simp add: Least_def)
  
-txt{*omit maybe?
+txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};