# HG changeset patch
# User huffman
# Date 1182462566 -7200
# Node ID 02099ea565554e594bebed542ef4c4194d3fbcc0
# Parent  08e6c03b2a726cd2419bd0cc0063811c649a27d9
section headings

diff -r 08e6c03b2a72 -r 02099ea56555 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Jun 21 23:33:10 2007 +0200
+++ b/src/HOL/Presburger.thy	Thu Jun 21 23:49:26 2007 +0200
@@ -3,6 +3,8 @@
    Author:     Amine Chaieb, TU Muenchen
 *)
 
+header {* Decision Procedure for Presburger Arithmetic *}
+
 theory Presburger
 imports Arith_Tools SetInterval
 uses
@@ -12,8 +14,6 @@
   ("Tools/Qelim/presburger.ML")
 begin
 
-subsection {* Decision Procedure for Presburger Arithmetic *}
-
 setup CooperData.setup
 
 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
@@ -62,7 +62,7 @@
   (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
     simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
 
-section{* The A and B sets *}
+subsection{* The A and B sets *}
 lemma bset:
   "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
      \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow>