equal
deleted
inserted
replaced
1632 of_int_floor_le of_rat_of_int_eq real_less_eq_code) |
1632 of_int_floor_le of_rat_of_int_eq real_less_eq_code) |
1633 |
1633 |
1634 |
1634 |
1635 text \<open>Quickcheck\<close> |
1635 text \<open>Quickcheck\<close> |
1636 |
1636 |
1637 definition (in term_syntax) |
1637 context |
|
1638 includes term_syntax |
|
1639 begin |
|
1640 |
|
1641 definition |
1638 valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" |
1642 valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" |
1639 where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k" |
1643 where [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k" |
|
1644 |
|
1645 end |
1640 |
1646 |
1641 instantiation real :: random |
1647 instantiation real :: random |
1642 begin |
1648 begin |
1643 |
1649 |
1644 context |
1650 context |