# HG changeset patch
# User haftmann
# Date 1177587189 -7200
# Node ID 5129e02f4df2c70ae269e99738f82bc6d7992aa2
# Parent  92026479179edc5d36c3c1b08875acf28ab7aed0
slightly tuned

diff -r 92026479179e -r 5129e02f4df2 src/HOL/Integ/NatBin.thy
--- 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
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Integ/NatSimprocs.thy
--- 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
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Integ/int_factor_simprocs.ML
--- 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);
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Integ/presburger.ML
--- 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]
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Library/AssocList.thy
--- 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
 *)
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Library/Pretty_Int.thy
--- 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
 *)
 
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Library/While_Combinator.thy
--- 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
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Real/rat_arith.ML
--- 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 *)
 
diff -r 92026479179e -r 5129e02f4df2 src/HOL/Tools/Presburger/presburger.ML
--- 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]
diff -r 92026479179e -r 5129e02f4df2 src/HOL/ex/Codegenerator_Rat.thy
--- 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