Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_Examples/Cantor.thy
changeset 69597 ff784d5a5bfb
parent 63680 6e1e8b5abbfa 
--- a/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -80,7 +80,7 @@
 
 text \<open>
   The following treatment of Cantor's Theorem follows the classic example from
-  the early 1990s, e.g.\ see the file @{verbatim "92/HOL/ex/set.ML"} in
+  the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
   Isabelle92 or @{cite \<open>\S18.7\<close> "paulson-isa-book"}. The old tactic scripts
   synthesize key information of the proof by refinement of schematic goal
   states. In contrast, the Isar proof needs to say explicitly what is proven.
isabelle