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/Quickcheck_Examples/Quickcheck_Interfaces.thy
changeset 69597 ff784d5a5bfb
parent 63167 0909deb8059b 
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -19,8 +19,8 @@
 \<close>
 
 ML \<open>
-val SOME testers = Quickcheck.mk_batch_validator @{context}
-  [@{term "x = (1 :: nat)"}, @{term "x = (0 :: nat)"}, @{term "x <= (5 :: nat)"}, @{term "0 \<le> (x :: nat)"}]
+val SOME testers = Quickcheck.mk_batch_validator \<^context>
+  [\<^term>\<open>x = (1 :: nat)\<close>, \<^term>\<open>x = (0 :: nat)\<close>, \<^term>\<open>x <= (5 :: nat)\<close>, \<^term>\<open>0 \<le> (x :: nat)\<close>]
 \<close>
 
 text \<open>
isabelle