src/HOL/ex/RPred.thy
changeset 42463 f270e3e18be5
parent 36176 3fe7e97ccca8
child 44845 5e51075cbd97
     1.1 --- a/src/HOL/ex/RPred.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/ex/RPred.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  imports Quickcheck Random Predicate
     1.5  begin
     1.6  
     1.7 -types 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
     1.8 +type_synonym 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
     1.9  
    1.10  section {* The RandomPred Monad *}
    1.11