src/HOL/RealDef.thy
changeset 43887 442aceb54969
parent 43733 a6ca7b83612f
child 44278 1220ecb81e8f
equal deleted inserted replaced
43886:bf068e758783 43887:442aceb54969
  1803 
  1803 
  1804 instance ..
  1804 instance ..
  1805 
  1805 
  1806 end
  1806 end
  1807 
  1807 
       
  1808 instantiation real :: narrowing
       
  1809 begin
       
  1810 
       
  1811 definition
       
  1812   "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"
       
  1813 
       
  1814 instance ..
       
  1815 
       
  1816 end
       
  1817 
       
  1818 
  1808 text {* Setup for SML code generator *}
  1819 text {* Setup for SML code generator *}
  1809 
  1820 
  1810 types_code
  1821 types_code
  1811   real ("(int */ int)")
  1822   real ("(int */ int)")
  1812 attach (term_of) {*
  1823 attach (term_of) {*