# HG changeset patch # User haftmann # Date 1256923960 -3600 # Node ID 2bd12592c5e852da941bbe4a5b13180bbc8b3298 # Parent 85adf83af7ce1c93b82984ee31f17eae0694110d tuned code setup diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Divides.thy Fri Oct 30 18:32:40 2009 +0100 @@ -131,7 +131,7 @@ note that ultimately show thesis by blast qed -lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \ b mod a = 0" +lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \ b mod a = 0" proof assume "b mod a = 0" with mod_div_equality [of b a] have "b div a * a = b" by simp @@ -2460,4 +2460,13 @@ then show ?thesis by (simp add: divmod_int_pdivmod) qed +code_modulename SML + Divides Arith + +code_modulename OCaml + Divides Arith + +code_modulename Haskell + Divides Arith + end diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/HOL.thy Fri Oct 30 18:32:40 2009 +0100 @@ -1818,7 +1818,7 @@ code_datatype "TYPE('a\{})" -code_datatype Trueprop "prop" +code_datatype "prop" Trueprop text {* Code equations *} diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Int.thy Fri Oct 30 18:32:40 2009 +0100 @@ -2246,13 +2246,13 @@ by simp code_modulename SML - Int Integer + Int Arith code_modulename OCaml - Int Integer + Int Arith code_modulename Haskell - Int Integer + Int Arith types_code "int" ("int") diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Oct 30 18:32:40 2009 +0100 @@ -424,22 +424,13 @@ text {* Module names *} code_modulename SML - Nat Integer - Divides Integer - Ring_and_Field Integer - Efficient_Nat Integer + Efficient_Nat Arith code_modulename OCaml - Nat Integer - Divides Integer - Ring_and_Field Integer - Efficient_Nat Integer + Efficient_Nat Arith code_modulename Haskell - Nat Integer - Divides Integer - Ring_and_Field Integer - Efficient_Nat Integer + Efficient_Nat Arith hide const int diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Nat.thy Fri Oct 30 18:32:40 2009 +0100 @@ -1674,4 +1674,16 @@ class size = fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded} *} + +subsection {* code module namespace *} + +code_modulename SML + Nat Arith + +code_modulename OCaml + Nat Arith + +code_modulename Haskell + Nat Arith + end diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/OrderedGroup.thy Fri Oct 30 18:32:40 2009 +0100 @@ -1409,4 +1409,13 @@ Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]; *} +code_modulename SML + OrderedGroup Arith + +code_modulename OCaml + OrderedGroup Arith + +code_modulename Haskell + OrderedGroup Arith + end diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Power.thy Fri Oct 30 18:32:40 2009 +0100 @@ -467,4 +467,13 @@ declare power.power.simps [code] +code_modulename SML + Power Arith + +code_modulename OCaml + Power Arith + +code_modulename Haskell + Power Arith + end diff -r 85adf83af7ce -r 2bd12592c5e8 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Oct 30 14:02:42 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Fri Oct 30 18:32:40 2009 +0100 @@ -2374,4 +2374,14 @@ then show ?thesis by simp qed + +code_modulename SML + Ring_and_Field Arith + +code_modulename OCaml + Ring_and_Field Arith + +code_modulename Haskell + Ring_and_Field Arith + end