equal
deleted
inserted
replaced
1741 |
1741 |
1742 definition (in term_syntax) |
1742 definition (in term_syntax) |
1743 valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1743 valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1744 [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k" |
1744 [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k" |
1745 |
1745 |
1746 notation fcomp (infixl "o>" 60) |
1746 notation fcomp (infixl "\<circ>>" 60) |
1747 notation scomp (infixl "o\<rightarrow>" 60) |
1747 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
1748 |
1748 |
1749 instantiation real :: random |
1749 instantiation real :: random |
1750 begin |
1750 begin |
1751 |
1751 |
1752 definition |
1752 definition |
1753 "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))" |
1753 "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))" |
1754 |
1754 |
1755 instance .. |
1755 instance .. |
1756 |
1756 |
1757 end |
1757 end |
1758 |
1758 |
1759 no_notation fcomp (infixl "o>" 60) |
1759 no_notation fcomp (infixl "\<circ>>" 60) |
1760 no_notation scomp (infixl "o\<rightarrow>" 60) |
1760 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
1761 |
1761 |
1762 text {* Setup for SML code generator *} |
1762 text {* Setup for SML code generator *} |
1763 |
1763 |
1764 types_code |
1764 types_code |
1765 real ("(int */ int)") |
1765 real ("(int */ int)") |