--- a/src/HOL/Integ/NatBin.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Integ/NatBin.thy Thu Apr 26 13:33:09 2007 +0200
@@ -15,7 +15,7 @@
*}
instance nat :: number
- nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))" ..
+ nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
abbreviation (xsymbols)
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
@@ -811,11 +811,6 @@
by (simp add: nat_mult_div_cancel1)
-subsection {* code generator setup *}
-
-lemmas [code inline] = nat_number_of_def
-
-
subsection {* legacy ML bindings *}
ML
@@ -832,7 +827,6 @@
val power2_minus = thm "power2_minus";
val power_minus1_even = thm "power_minus1_even";
val power_minus_even = thm "power_minus_even";
-(* val zero_le_even_power = thm "zero_le_even_power"; *)
val odd_power_less_zero = thm "odd_power_less_zero";
val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
@@ -889,7 +883,6 @@
val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
val power_minus_even = thm"power_minus_even";
-(* val zero_le_even_power = thm"zero_le_even_power"; *)
*}
end
--- a/src/HOL/Integ/NatSimprocs.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Thu Apr 26 13:33:09 2007 +0200
@@ -383,10 +383,9 @@
"[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
by (unfold dvd_def) auto
-ML
-{*
-val divide_minus1 = thm "divide_minus1";
-val minus1_divide = thm "minus1_divide";
+ML {*
+val divide_minus1 = @{thm divide_minus1};
+val minus1_divide = @{thm minus1_divide};
*}
end
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Thu Apr 26 13:33:09 2007 +0200
@@ -24,7 +24,7 @@
(** Factor cancellation theorems for integer division (div, not /) **)
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
-by (stac zdiv_zmult_zmult1 1);
+by (stac @{thm zdiv_zmult_zmult1} 1);
by Auto_tac;
qed "int_mult_div_cancel1";
@@ -236,7 +236,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
- [@{thm mult_1_left}, mult_1_right, zdiv_1, numeral_1_eq_1];
+ [@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
--- a/src/HOL/Integ/presburger.ML Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Integ/presburger.ML Thu Apr 26 13:33:09 2007 +0200
@@ -93,13 +93,13 @@
val nat_mod_add_eq = mod_add1_eq RS sym;
val nat_mod_add_left_eq = mod_add_left_eq RS sym;
val nat_mod_add_right_eq = mod_add_right_eq RS sym;
-val int_mod_add_eq = zmod_zadd1_eq RS sym;
-val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
-val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
-val nat_div_add_eq = div_add1_eq RS sym;
-val int_div_add_eq = zdiv_zadd1_eq RS sym;
-val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
+val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
+val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
+val nat_div_add_eq = @{thm div_add1_eq} RS sym;
+val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
+val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
+val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
(* extract all the constants in a term*)
@@ -292,11 +292,11 @@
nat_mod_add_right_eq, int_mod_add_eq,
int_mod_add_right_eq, int_mod_add_left_eq,
nat_div_add_eq, int_div_add_eq,
- mod_self, zmod_self,
+ mod_self, @{thm zmod_self},
DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
- zdiv_zero,zmod_zero,div_0,mod_0,
- zdiv_1,zmod_1,div_1,mod_1,
+ @{thm zdiv_zero}, @{thm zmod_zero}, div_0,mod_0,
+ @{thm zdiv_1}, @{thm zmod_1}, @{thm div_1}, @{thm mod_1},
Suc_plus1]
addsimps add_ac
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Library/AssocList.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Library/AssocList.thy Thu Apr 26 13:33:09 2007 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Library.thy
+(* Title: HOL/Library/AssocList.thy
ID: $Id$
Author: Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
*)
--- a/src/HOL/Library/Pretty_Int.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Library/Pretty_Int.thy Thu Apr 26 13:33:09 2007 +0200
@@ -1,4 +1,5 @@
-(* ID: $Id$
+(* Title: HOL/Library/Pretty_Int.thy
+ ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/Library/While_Combinator.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Library/While_Combinator.thy Thu Apr 26 13:33:09 2007 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/While.thy
+(* Title: HOL/Library/While_Combinator.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TU Muenchen
--- a/src/HOL/Real/rat_arith.ML Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML Thu Apr 26 13:33:09 2007 +0200
@@ -17,16 +17,16 @@
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
- of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
- of_int_mult, of_int_of_nat_eq]
+ of_int_0, of_int_1, @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
+ @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
-val nat_inj_thms = [of_nat_le_iff RS iffD2,
- of_nat_eq_iff RS iffD2]
+val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
+ @{thm of_nat_eq_iff} RS iffD2]
(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
of_nat_less_iff RS iffD2 *)
-val int_inj_thms = [of_int_le_iff RS iffD2,
- of_int_eq_iff RS iffD2]
+val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
+ @{thm of_int_eq_iff} RS iffD2]
(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
of_int_less_iff RS iffD2 *)
--- a/src/HOL/Tools/Presburger/presburger.ML Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Apr 26 13:33:09 2007 +0200
@@ -93,13 +93,13 @@
val nat_mod_add_eq = mod_add1_eq RS sym;
val nat_mod_add_left_eq = mod_add_left_eq RS sym;
val nat_mod_add_right_eq = mod_add_right_eq RS sym;
-val int_mod_add_eq = zmod_zadd1_eq RS sym;
-val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
-val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
-val nat_div_add_eq = div_add1_eq RS sym;
-val int_div_add_eq = zdiv_zadd1_eq RS sym;
-val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
-val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
+val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
+val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
+val nat_div_add_eq = @{thm div_add1_eq} RS sym;
+val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
+val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
+val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
(* extract all the constants in a term*)
@@ -292,11 +292,11 @@
nat_mod_add_right_eq, int_mod_add_eq,
int_mod_add_right_eq, int_mod_add_left_eq,
nat_div_add_eq, int_div_add_eq,
- mod_self, zmod_self,
+ mod_self, @{thm zmod_self},
DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
- zdiv_zero,zmod_zero,div_0,mod_0,
- zdiv_1,zmod_1,div_1,mod_1,
+ @{thm zdiv_zero}, @{thm zmod_zero}, div_0,mod_0,
+ @{thm zdiv_1}, @{thm zmod_1}, @{thm div_1}, @{thm mod_1},
Suc_plus1]
addsimps add_ac
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/ex/Codegenerator_Rat.thy Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Rat.thy Thu Apr 26 13:33:09 2007 +0200
@@ -6,7 +6,7 @@
header {* Simple example for executable rational numbers *}
theory Codegenerator_Rat
-imports EfficientNat ExecutableRat
+imports ExecutableRat EfficientNat
begin
definition
@@ -29,7 +29,7 @@
definition
"foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
-code_gen foobar (SML #) (SML -)
+code_gen foobar (SML #) (OCaml -) (Haskell -)
ML {* ROOT.Codegenerator_Rat.foobar *}
code_module Foo