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/ex/Refute_Examples.thy
changeset 69597 ff784d5a5bfb
parent 67613 ce654b0e6d69 
--- a/src/HOL/ex/Refute_Examples.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -15,8 +15,8 @@
 
 lemma "P \<and> Q"
 apply (rule conjI)
-refute [expect = genuine] 1  \<comment> \<open>refutes @{term "P"}\<close>
-refute [expect = genuine] 2  \<comment> \<open>refutes @{term "Q"}\<close>
+refute [expect = genuine] 1  \<comment> \<open>refutes \<^term>\<open>P\<close>\<close>
+refute [expect = genuine] 2  \<comment> \<open>refutes \<^term>\<open>Q\<close>\<close>
 refute [expect = genuine]    \<comment> \<open>equivalent to 'refute 1'\<close>
   \<comment> \<open>here 'refute 3' would cause an exception, since we only have 2 subgoals\<close>
 refute [maxsize = 5, expect = genuine]   \<comment> \<open>we can override parameters ...\<close>
@@ -472,7 +472,7 @@
 
 subsubsection \<open>Subtypes (typedef), typedecl\<close>
 
-text \<open>A completely unspecified non-empty subset of @{typ "'a"}:\<close>
+text \<open>A completely unspecified non-empty subset of \<^typ>\<open>'a\<close>:\<close>
 
 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
 
@@ -704,8 +704,8 @@
 
 lemma "P Suc"
 refute [maxsize = 3, expect = none]
-\<comment> \<open>@{term Suc} is a partial function (regardless of the size
-      of the model), hence @{term "P Suc"} is undefined and no
+\<comment> \<open>\<^term>\<open>Suc\<close> is a partial function (regardless of the size
+      of the model), hence \<^term>\<open>P Suc\<close> is undefined and no
       model will be found\<close>
 oops
isabelle