equal
deleted
inserted
replaced
1011 instantiation rat :: random |
1011 instantiation rat :: random |
1012 begin |
1012 begin |
1013 |
1013 |
1014 definition |
1014 definition |
1015 "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair ( |
1015 "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair ( |
1016 let j = Code_Index.int_of (denom + 1) |
1016 let j = Code_Numeral.int_of (denom + 1) |
1017 in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))" |
1017 in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))" |
1018 |
1018 |
1019 instance .. |
1019 instance .. |
1020 |
1020 |
1021 end |
1021 end |