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.thy
changeset 42163 392fd6c4669c
parent 42159 234ec7011e5d
child 42175 32c3bb5e1b1a 
--- a/src/HOL/Quickcheck.thy	Wed Mar 30 11:32:51 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Mar 30 11:32:52 2011 +0200
@@ -164,7 +164,7 @@
    in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
 unfolding iter_def iter'.simps[of _ nrandom] ..
 
-types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
 
 definition empty :: "'a randompred"
   where "empty = Pair (bot_class.bot)"
isabelle