# 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 "-\"} and @{text "+\"} 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: "\\x.(\j \ {1 .. D}. \b\B. x \ b + j)\ P x \ P(x - D) ; \x.(\j\{1 .. D}. \b\B. x \ b + j)\ Q x \ Q(x - D)\ \