src/HOL/Metis_Examples/Tarski.thy

--- a/src/HOL/Metis_Examples/Tarski.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -461,7 +461,7 @@
 (*never proved, 2007-01-22*)
 apply (rule transE)
 -- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *}
--- {* because of the def of @{text H} *}
+-- {* because of the definition of @{text H} *}
 apply fast
 -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
 apply (rule_tac f = "f" in monotoneE)