equal
deleted
inserted
replaced
134 by (auto simp add: select_weight_def select_def scomp_def split_def |
134 by (auto simp add: select_weight_def select_def scomp_def split_def |
135 fun_eq_iff pick_same [symmetric] less_natural_def) |
135 fun_eq_iff pick_same [symmetric] less_natural_def) |
136 qed |
136 qed |
137 |
137 |
138 |
138 |
139 subsection \<open>@{text ML} interface\<close> |
139 subsection \<open>\<open>ML\<close> interface\<close> |
140 |
140 |
141 code_reflect Random_Engine |
141 code_reflect Random_Engine |
142 functions range select select_weight |
142 functions range select select_weight |
143 |
143 |
144 ML \<open> |
144 ML \<open> |