# HG changeset patch
# User haftmann
# Date 1238145175 -3600
# Node ID 9e23e3ea7eddb6603edd576f21cf7dc477a0de6c
# Parent  f5d9cc53f4c8ccd7fd90a11041831c77d485a77b# Parent  2d3ae5a7edb23e933135f5b65a71b55629f8b49d
merged

diff -r f5d9cc53f4c8 -r 9e23e3ea7edd NEWS
--- a/NEWS	Fri Mar 27 09:58:48 2009 +0100
+++ b/NEWS	Fri Mar 27 10:12:55 2009 +0100
@@ -502,10 +502,9 @@
 resulting ML value/function/datatype constructor binding in place.
 All occurrences of @{code} with a single ML block are generated
 simultaneously.  Provides a generic and safe interface for
-instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
-example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
-application.  In future you ought refrain from ad-hoc compiling
-generated SML code on the ML toplevel.  Note that (for technical
+instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for
+a more ambitious application.  In future you ought refrain from ad-hoc
+compiling generated SML code on the ML toplevel.  Note that (for technical
 reasons) @{code} cannot refer to constants for which user-defined
 serializations are set.  Refer to the corresponding ML counterpart
 directly in that cases.
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -6,7 +6,7 @@
   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
-imports Plain Groebner_Basis Main
+imports Main
 uses
   "~~/src/HOL/Tools/Qelim/langford_data.ML"
   "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/GCD.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -6,7 +6,7 @@
 header {* The Greatest Common Divisor *}
 
 theory GCD
-imports Plain Presburger Main
+imports Main
 begin
 
 text {*
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Heap.thy
-    ID:         $Id$
     Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
 *)
 
 header {* A polymorphic heap based on cantor encodings *}
 
 theory Heap
-imports Plain "~~/src/HOL/List" Countable Typerep
+imports Main Countable
 begin
 
 subsection {* Representable types *}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -5,7 +5,7 @@
 header {* Permutations *}
 
 theory Permutation
-imports Plain Multiset
+imports Main Multiset
 begin
 
 inductive
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Pocklington.thy
--- a/src/HOL/Library/Pocklington.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,13 +1,11 @@
 (*  Title:      HOL/Library/Pocklington.thy
-    ID:         $Id$
     Author:     Amine Chaieb
 *)
 
 header {* Pocklington's Theorem for Primes *}
 
-
 theory Pocklington
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
+imports Main Primes
 begin
 
 definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -6,7 +6,7 @@
 header {* Univariate Polynomials *}
 
 theory Polynomial
-imports Plain SetInterval Main
+imports Main
 begin
 
 subsection {* Definition of type @{text poly} *}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Primes.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -6,7 +6,7 @@
 header {* Primality on nat *}
 
 theory Primes
-imports Plain "~~/src/HOL/ATP_Linkup" "~~/src/HOL/GCD" "~~/src/HOL/Parity"
+imports Complex_Main
 begin
 
 definition
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Product_ord.thy
-    ID:         $Id$
     Author:     Norbert Voelker
 *)
 
 header {* Order on product types *}
 
 theory Product_ord
-imports Plain
+imports Main
 begin
 
 instantiation "*" :: (ord, ord) ord
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,12 +1,11 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow
+(*  Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 *)
 
 header{*Quicksort*}
 
 theory Quicksort
-imports Plain Multiset
+imports Main Multiset
 begin
 
 context linorder
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Quotient.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Quotient.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Quotient types *}
 
 theory Quotient
-imports Plain "~~/src/HOL/Hilbert_Choice"
+imports Main
 begin
 
 text {*
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      RBT.thy
-    ID:         $Id$
     Author:     Markus Reiter, TU Muenchen
     Author:     Alexander Krauss, TU Muenchen
 *)
@@ -8,7 +7,7 @@
 
 (*<*)
 theory RBT
-imports Plain AssocList
+imports Main AssocList
 begin
 
 datatype color = R | B
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Ramsey.thy
-    ID:         $Id$
     Author:     Tom Ridge. Converted to structured Isar by L C Paulson
 *)
 
 header "Ramsey's Theorem"
 
 theory Ramsey
-imports Plain "~~/src/HOL/Presburger" Infinite_Set
+imports Main Infinite_Set
 begin
 
 subsection {* Preliminaries *}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -5,7 +5,7 @@
 header {* Operations on sets and functions *}
 
 theory SetsAndFunctions
-imports Plain
+imports Main
 begin
 
 text {*
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 subsection {* Motivation *}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,13 +1,12 @@
 (*  Title:      HOL/Library/Sublist_Order.thy
-    ID:         $Id$
     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
-                Florian Haftmann, TU München
+                Florian Haftmann, TU Muenchen
 *)
 
 header {* Sublist Ordering *}
 
 theory Sublist_Order
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 text {*
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -5,7 +5,7 @@
 header {* Univariate Polynomials *}
 
 theory Univ_Poly
-imports Plain List
+imports Main
 begin
 
 text{* Application of polynomial as a function. *}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/While_Combinator.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TU Muenchen
 *)
@@ -7,7 +6,7 @@
 header {* A general ``while'' combinator *}
 
 theory While_Combinator
-imports Plain "~~/src/HOL/Presburger"
+imports Main
 begin
 
 text {* 
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Lubs.thy
--- a/src/HOL/Lubs.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Lubs.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -6,7 +6,7 @@
 header{*Definitions of Upper Bounds and Least Upper Bounds*}
 
 theory Lubs
-imports Plain Main
+imports Main
 begin
 
 text{*Thanks to suggestions by James Margetson*}
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Map.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Map.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, based on a theory by David von Oheimb
     Copyright   1997-2003 TU Muenchen
 
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Parity.thy	Fri Mar 27 10:12:55 2009 +0100
@@ -5,7 +5,7 @@
 header {* Even and Odd for int and nat *}
 
 theory Parity
-imports Plain Presburger Main
+imports Main
 begin
 
 class even_odd = 
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 27 10:12:55 2009 +0100
@@ -79,10 +79,7 @@
    in lhs aconv rhs end
    handle U.ERR _ => false;
    
-
-fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]);
-val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
-val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
+val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
 fun mk_meta_eq r = case concl_of r of
      Const("==",_)$_$_ => r
   |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/ex/Code_Antiq.thy
--- a/src/HOL/ex/Code_Antiq.thy	Fri Mar 27 09:58:48 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(*  Title:      HOL/ex/Code_Antiq.thy
-    ID:         $Id$
-    Author:     Florian Haftmann
-*)
-
-header {* A simple certificate check as toy example for the code antiquotation *}
-
-theory Code_Antiq
-imports Plain
-begin
-
-lemma div_cert1:
-  fixes n m q r :: nat
-  assumes "r < m"
-    and "0 < m"
-    and "n = m * q + r"
-  shows "n div m = q"
-using assms by (simp add: div_mult_self2 add_commute)
-
-lemma div_cert2:
-  fixes n :: nat
-  shows "n div 0 = 0"
-by simp
-
-ML {*
-local
-
-fun code_of_val k = if k <= 0 then @{code "0::nat"}
-  else @{code Suc} (code_of_val (k - 1));
-
-fun val_of_code @{code "0::nat"} = 0
-  | val_of_code (@{code Suc} n) = val_of_code n + 1;
-
-val term_of_code = HOLogic.mk_nat o val_of_code;
-
-infix 9 &$;
-val op &$ = uncurry Thm.capply;
-
-val simpset = HOL_ss addsimps
-  @{thms plus_nat.simps add_0_right add_Suc_right times_nat.simps mult_0_right mult_Suc_right  less_nat_zero_code le_simps(2) less_eq_nat.simps(1) le_simps(3)}
-
-fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
-  (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
-
-in
-
-fun simp_div ctxt ct_n ct_m =
-  let
-    val m = HOLogic.dest_nat (Thm.term_of ct_m);
-  in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
-    let
-      val thy = ProofContext.theory_of ctxt;
-      val n = HOLogic.dest_nat (Thm.term_of ct_n);
-      val c_n = code_of_val n;
-      val c_m = code_of_val m;
-      val (c_q, c_r) = @{code divmod} c_n c_m;
-      val t_q = term_of_code c_q;
-      val t_r = term_of_code c_r;
-      val ct_q = Thm.cterm_of thy t_q;
-      val ct_r = Thm.cterm_of thy t_r;
-      val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
-      val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
-      val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
-        &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
-          &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
-    in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
-  end;
-
-end;
-*}
-
-ML_val {*
-  simp_div @{context}
-    @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
-    @{cterm "(Suc (Suc 0))"}
-*}
-
-ML_val {*
-  simp_div @{context}
-    (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
-    (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
-*}
-
-end
\ No newline at end of file
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 27 10:12:55 2009 +0100
@@ -56,7 +56,6 @@
   "Classical",
   "set",
   "Meson_Test",
-  "Code_Antiq",
   "Termination",
   "Coherent",
   "PresburgerEx",
diff -r f5d9cc53f4c8 -r 9e23e3ea7edd src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Fri Mar 27 09:58:48 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Fri Mar 27 10:12:55 2009 +0100
@@ -215,9 +215,10 @@
           |> Conjunction.elim_balanced (length thms)
   in
     thms
-    |> burrow_thms (canonical_tvars thy purify_tvar)
     |> map (canonical_vars thy purify_var)
     |> map (canonical_absvars purify_var)
+    |> map Drule.zero_var_indexes
+    |> burrow_thms (canonical_tvars thy purify_tvar)
     |> Drule.zero_var_indexes_list
   end;