src/HOL/ex/Numeral.thy
changeset 37826 4c0a5e35931a
parent 37765 26bdfb7b680b
child 38054 acd48ef85bfc
equal deleted inserted replaced
37825:adc1143bc1a8 37826:4c0a5e35931a
   986 
   986 
   987 
   987 
   988 subsection {* Toy examples *}
   988 subsection {* Toy examples *}
   989 
   989 
   990 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
   990 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
       
   991 
   991 code_thms bar
   992 code_thms bar
   992 export_code bar in Haskell file -
   993 
   993 export_code bar in OCaml module_name Foo file -
   994 export_code bar checking SML OCaml? Haskell?
   994 ML {* @{code bar} *}
   995 
   995 
   996 end
   996 end