--- a/src/HOL/Commutative_Ring.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/Commutative_Ring.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,31 +1,32 @@
-
(* ID: $Id$
Author: Bernhard Haeupler
- Proving equalities in a commutative Ring done "right" in Isabelle/HOL
+Proving equalities in commutative rings done "right" in Isabelle/HOL.
*)
+header {* Proving equalities in commutative rings *}
+
theory Commutative_Ring
imports List
uses ("Tools/comm_ring.ML")
begin
(* Syntax of multivariate polynomials (pol) and polynomial expressions*)
-datatype 'a pol =
- Pc 'a
- | Pinj nat "'a pol"
+datatype 'a pol =
+ Pc 'a
+ | Pinj nat "'a pol"
| PX "'a pol" nat "'a pol"
-datatype 'a polex =
- Pol "'a pol"
- | Add "'a polex" "'a polex"
- | Sub "'a polex" "'a polex"
- | Mul "'a polex" "'a polex"
+datatype 'a polex =
+ Pol "'a pol"
+ | Add "'a polex" "'a polex"
+ | Sub "'a polex" "'a polex"
+ | Mul "'a polex" "'a polex"
| Pow "'a polex" nat
| Neg "'a polex"
(* Interpretation functions for the shadow syntax *)
-consts
+consts
Ipol :: "('a::{comm_ring,recpower}) list \<Rightarrow> 'a pol \<Rightarrow> 'a"
Ipolex :: "('a::{comm_ring,recpower}) list \<Rightarrow> 'a polex \<Rightarrow> 'a"
@@ -44,7 +45,7 @@
(* Create polynomial normalized polynomials given normalized inputs *)
constdefs mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
- mkPinj_def: "mkPinj x P \<equiv> (case P of
+ mkPinj_def: "mkPinj x P \<equiv> (case P of
(Pc c) \<Rightarrow> (Pc c) |
(Pinj y P) \<Rightarrow> Pinj (x+y) P |
(PX p1 y p2) \<Rightarrow> Pinj x P )"
@@ -71,21 +72,21 @@
"add (Pinj i P, Pc c) = Pinj i (add (P, Pc c))"
"add (Pc c, PX P i Q) = PX P i (add (Q, Pc c))"
"add (PX P i Q, Pc c) = PX P i (add (Q, Pc c))"
- "add (Pinj x P, Pinj y Q) =
- (if x=y then mkPinj x (add (P, Q))
+ "add (Pinj x P, Pinj y Q) =
+ (if x=y then mkPinj x (add (P, Q))
else (if x>y then mkPinj y (add (Pinj (x-y) P, Q))
else mkPinj x (add (Pinj (y-x) Q, P)) ))"
- "add (Pinj x P, PX Q y R) =
- (if x=0 then add(P, PX Q y R)
- else (if x=1 then PX Q y (add (R, P))
+ "add (Pinj x P, PX Q y R) =
+ (if x=0 then add(P, PX Q y R)
+ else (if x=1 then PX Q y (add (R, P))
else PX Q y (add (R, Pinj (x - 1) P))))"
- "add (PX P x R, Pinj y Q) =
- (if y=0 then add(PX P x R, Q)
- else (if y=1 then PX P x (add (R, Q))
+ "add (PX P x R, Pinj y Q) =
+ (if y=0 then add(PX P x R, Q)
+ else (if y=1 then PX P x (add (R, Q))
else PX P x (add (R, Pinj (y - 1) Q))))"
- "add (PX P1 x P2, PX Q1 y Q2) =
- (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2))
- else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2))
+ "add (PX P1 x P2, PX Q1 y Q2) =
+ (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2))
+ else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2))
else mkPX (add (PX Q1 (y-x) (Pc 0), P1)) x (add (P2,Q2)) ))"
(* Multiplication *)
@@ -93,24 +94,24 @@
"mul (Pc a, Pc b) = Pc (a*b)"
"mul (Pc c, Pinj i P) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
"mul (Pinj i P, Pc c) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
- "mul (Pc c, PX P i Q) =
+ "mul (Pc c, PX P i Q) =
(if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
- "mul (PX P i Q, Pc c) =
+ "mul (PX P i Q, Pc c) =
(if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
- "mul (Pinj x P, Pinj y Q) =
- (if x=y then mkPinj x (mul (P, Q))
+ "mul (Pinj x P, Pinj y Q) =
+ (if x=y then mkPinj x (mul (P, Q))
else (if x>y then mkPinj y (mul (Pinj (x-y) P, Q))
else mkPinj x (mul (Pinj (y-x) Q, P)) ))"
- "mul (Pinj x P, PX Q y R) =
- (if x=0 then mul(P, PX Q y R)
- else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P))
+ "mul (Pinj x P, PX Q y R) =
+ (if x=0 then mul(P, PX Q y R)
+ else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P))
else mkPX (mul (Pinj x P, Q)) y (mul (R, Pinj (x - 1) P))))"
- "mul (PX P x R, Pinj y Q) =
- (if y=0 then mul(PX P x R, Q)
- else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q))
+ "mul (PX P x R, Pinj y Q) =
+ (if y=0 then mul(PX P x R, Q)
+ else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q))
else mkPX (mul (Pinj y Q, P)) x (mul (R, Pinj (y - 1) Q))))"
- "mul (PX P1 x P2, PX Q1 y Q2) =
- add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)),
+ "mul (PX P1 x P2, PX Q1 y Q2) =
+ add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)),
add (mkPX (mul (P1, mkPinj 1 Q2)) x (Pc 0), mkPX (mul (Q1, mkPinj 1 P2)) y (Pc 0)) )"
(hints simp add: mkPinj_def split: pol.split)
@@ -146,16 +147,16 @@
lemma number_of_nat_even: "even (number_of (w BIT bit.B0)::nat)"
by simp
-
+
lemma pow_even : "pow (p, number_of(w BIT bit.B0)) = pow (sqr p, number_of w)"
( is "pow(?p,?n) = pow (_,?n2)")
proof-
have "even ?n" by simp
- hence "pow (p, ?n) = pow (sqr p, ?n div 2)"
+ hence "pow (p, ?n) = pow (sqr p, ?n div 2)"
apply simp
apply (cases "IntDef.neg (number_of w)")
apply simp
- done
+ done
*)
(* Normalization of polynomial expressions *)
@@ -197,7 +198,7 @@
then obtain d where "d+y=x"..
with prems have ?case by (auto simp add: mkPinj_ci ring_eq_simps) }
ultimately show ?case by blast
-next
+next
case (7 x P Q y R)
have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
moreover
@@ -219,7 +220,7 @@
then obtain d where "d+1=y" ..
with prems have ?case by auto }
ultimately show ?case by blast
-next
+next
case (9 P1 x P2 Q1 y Q2)
have "y < x \<or> x = y \<or> x < y" by arith
moreover
@@ -236,8 +237,8 @@
qed (auto simp add: ring_eq_simps)
(* Multiplication *)
-lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
- by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
+lemma mul_ci: "ALL l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
+ by (induct P Q rule: mul.induct, auto simp add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
(* Substraction *)
lemma sub_ci: "\<forall> l. Ipol l (sub p q) = (Ipol l p) - (Ipol l q)"
@@ -254,7 +255,7 @@
proof(induct n rule: nat_less_induct)
case (1 k)
have two:"2=Suc( Suc 0)" by simp
- from prems show ?case
+ from prems show ?case
proof(cases k)
case (Suc l)
hence KL:"k=Suc l" by simp
@@ -272,12 +273,12 @@
{assume OL:"odd l"
with prems have "\<lbrakk>\<forall>m<Suc l. \<forall>p. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\<rbrakk> \<Longrightarrow> \<forall>p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"
proof(cases l)
- case (Suc w)
- from prems have EW:"even w" by simp
- from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW])
- have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc)
- from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp
- with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
+ case (Suc w)
+ from prems have EW:"even w" by simp
+ from two have two_times:"(2 * (w div 2))= w" by (simp only: even_nat_div_two_times_two[OF EW])
+ have A:"ALL p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))" by (simp add: power_Suc)
+ from A two[symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2" by simp
+ with prems show ?thesis by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
qed(simp)
with prems have ?thesis by simp }
ultimately show ?thesis by blast
@@ -290,7 +291,7 @@
(* Reflection lemma: Key to the (incomplete) decision procedure *)
lemma norm_eq:
- assumes A:"norm P1 = norm P2"
+ assumes A:"norm P1 = norm P2"
shows "Ipolex l P1 = Ipolex l P2"
proof -
from A have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
@@ -303,8 +304,7 @@
Does not work, since no generic ring operations implementation is there
generate_code ("ring.ML") test = "norm"*)
-
- use "Tools/comm_ring.ML"
+use "Tools/comm_ring.ML"
setup "CommRing.setup"
end
--- a/src/HOL/ex/Adder.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Adder.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,11 +1,9 @@
(* Title: HOL/ex/Adder.thy
ID: $Id$
Author: Sergey Tverdyshev (Universitaet des Saarlandes)
-
-Implementation of carry chain incrementor and adder.
*)
-header{* Adder *}
+header {* Implementation of carry chain incrementor and adder *}
theory Adder imports Main Word begin
--- a/src/HOL/ex/CTL.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/CTL.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,4 +1,3 @@
-
(* Title: HOL/ex/CTL.thy
ID: $Id$
Author: Gertrud Bauer
@@ -8,8 +7,6 @@
theory CTL imports Main begin
-
-
text {*
We formalize basic concepts of Computational Tree Logic (CTL)
\cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
--- a/src/HOL/ex/Commutative_RingEx.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Commutative_RingEx.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,10 +1,13 @@
- (* $Id$ *)
+(* ID: $Id$
+ Author: Bernhard Haeupler
+*)
+
+header {* Some examples demonstrating the comm-ring method *}
+
theory Commutative_RingEx
imports Main
begin
- (* Some examples demonstrating the comm_ring method *)
-
lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
by comm_ring
@@ -44,4 +47,4 @@
lemma "(a::int)^10 - b^10 = (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9 )"
by comm_ring
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,9 +1,12 @@
(* ID: $Id$
Author: Bernhard Haeupler
- This theory is about the relative completeness of the tactic
- As long as the reified atomic polynomials of type 'a pol
- are in normal form, the cring method is complete *)
+This theory is about of the relative completeness of method comm-ring
+method. As long as the reified atomic polynomials of type 'a pol are
+in normal form, the cring method is complete.
+*)
+
+header {* Proof of the relative completeness of method comm-ring *}
theory Commutative_Ring_Complete
imports Main
@@ -381,4 +384,4 @@
qed(simp)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/InductiveInvariant.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,12 +1,15 @@
+(* ID: $Id$
+ Author: Sava Krsti\'{c} and John Matthews
+*)
+
+header {* Some of the results in Inductive Invariants for Nested Recursion *}
+
theory InductiveInvariant imports Main begin
-(** Authors: Sava Krsti\'{c} and John Matthews **)
-(** Date: Sep 12, 2003 **)
-
-text {* A formalization of some of the results in
- \emph{Inductive Invariants for Nested Recursion},
- by Sava Krsti\'{c} and John Matthews.
- Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *}
+text {* A formalization of some of the results in \emph{Inductive
+ Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
+ Matthews. Appears in the proceedings of TPHOLs 2003, LNCS
+ vol. 2758, pp. 253-269. *}
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
@@ -86,4 +89,4 @@
==> S x (f x)"
by (simp add: indinv_on_wfrec)
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,7 +1,10 @@
-theory InductiveInvariant_examples imports InductiveInvariant begin
+(* ID: $Id$
+ Author: Sava Krsti\'{c} and John Matthews
+*)
-(** Authors: Sava Krsti\'{c} and John Matthews **)
-(** Date: Oct 17, 2003 **)
+header {* Example use if an inductive invariant to solve termination conditions *}
+
+theory InductiveInvariant_examples imports InductiveInvariant begin
text "A simple example showing how to use an inductive invariant
to solve termination conditions generated by recdef on
@@ -124,4 +127,4 @@
by (subst ninety_one.simps,
simp add: ninety_one_tc measure_def inv_image_def)
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Intuitionistic.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Intuitionistic.thy Wed Sep 14 22:08:08 2005 +0200
@@ -3,11 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Higher-Order Logic: Intuitionistic predicate calculus problems
-
Taken from FOL/ex/int.ML
*)
+header {* Higher-Order Logic: Intuitionistic predicate calculus problems *}
+
theory Intuitionistic imports Main begin
--- a/src/HOL/ex/Lagrange.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Lagrange.thy Wed Sep 14 22:08:08 2005 +0200
@@ -2,28 +2,31 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1996 TU Muenchen
-
-
-This theory only contains a single theorem, which is a lemma in Lagrange's
-proof that every natural number is the sum of 4 squares. Its sole purpose is
-to demonstrate ordered rewriting for commutative rings.
-
-The enterprising reader might consider proving all of Lagrange's theorem.
*)
+header {* A lemma for Lagrange's theorem *}
+
theory Lagrange imports Main begin
+text {* This theory only contains a single theorem, which is a lemma
+in Lagrange's proof that every natural number is the sum of 4 squares.
+Its sole purpose is to demonstrate ordered rewriting for commutative
+rings.
+
+The enterprising reader might consider proving all of Lagrange's
+theorem. *}
+
constdefs sq :: "'a::times => 'a"
"sq x == x*x"
-(* The following lemma essentially shows that every natural number is the sum
-of four squares, provided all prime numbers are. However, this is an
-abstract theorem about commutative rings. It has, a priori, nothing to do
-with nat.*)
+text {* The following lemma essentially shows that every natural
+number is the sum of four squares, provided all prime numbers are.
+However, this is an abstract theorem about commutative rings. It has,
+a priori, nothing to do with nat. *}
ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
-(*once a slow step, but now (2001) just three seconds!*)
+-- {* once a slow step, but now (2001) just three seconds! *}
lemma Lagrange_lemma:
"!!x1::'a::comm_ring.
(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
@@ -36,7 +39,6 @@
text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
-(*
lemma "!!p1::'a::comm_ring.
(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
@@ -48,6 +50,8 @@
sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
+oops
+(*
by(simp add: sq_def ring_eq_simps)
*)
--- a/src/HOL/ex/Locales.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Locales.thy Wed Sep 14 22:08:08 2005 +0200
@@ -3,7 +3,7 @@
Author: Markus Wenzel, LMU München
*)
-header {* Using locales in Isabelle/Isar *}
+header {* Using locales in Isabelle/Isar -- outdated version! *}
theory Locales imports Main begin
--- a/src/HOL/ex/MonoidGroup.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/MonoidGroup.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,11 +1,9 @@
(* Title: HOL/ex/MonoidGroup.thy
ID: $Id$
Author: Markus Wenzel
-
-Monoids and Groups as predicates over record schemes.
*)
-header {* Monoids and Groups *}
+header {* Monoids and Groups as predicates over record schemes *}
theory MonoidGroup imports Main begin
--- a/src/HOL/ex/PresburgerEx.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/PresburgerEx.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,9 +1,9 @@
(* Title: HOL/ex/PresburgerEx.thy
ID: $Id$
Author: Amine Chaieb, TU Muenchen
+*)
-Some examples for Presburger Arithmetic
-*)
+header {* Some examples for Presburger Arithmetic *}
theory PresburgerEx imports Main begin
--- a/src/HOL/ex/Puzzle.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Puzzle.thy Wed Sep 14 22:08:08 2005 +0200
@@ -8,6 +8,8 @@
Proof due to Herbert Ehler
*)
+header {* A question from ``Bundeswettbewerb Mathematik'' *}
+
theory Puzzle imports Main begin
consts f :: "nat => nat"
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Sep 14 22:08:08 2005 +0200
@@ -144,5 +144,3 @@
oops
end
-
-
--- a/src/HOL/ex/Reflected_Presburger.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,10 +1,15 @@
-(* A formalization of quantifier elimination for Presburger arithmetic*)
-(* based on a generic quantifier elimination algorithm and
- cooper's methos to eliminate on \<exists> *)
+(* Title: HOL/ex/PresburgerEx.thy
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+
+A formalization of quantifier elimination for Presburger arithmetic
+based on a generic quantifier elimination algorithm and Cooper's
+methos to eliminate on \<exists>. *)
+
+header {* Quantifier elimination for Presburger arithmetic *}
theory Reflected_Presburger
imports Main
-(* uses ("rcooper.ML") ("rpresbtac.ML") *)
begin
(* Shadow syntax for integer terms *)
@@ -2051,7 +2056,6 @@
and dvd: "i dvd l"
shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
proof-
- thm dvd_div_pos[OF lpos inz dvd]
have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
have ldivinz: "l div i \<noteq> 0" using inz ldvdii lpos by auto
have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)"
@@ -2224,7 +2228,6 @@
assume nz: "n=0"
from prems have inz: "i \<noteq> 0" by auto
from prems nz have idvdl: "i dvd l" by simp
- thm adjustcoeff_eq_corr[OF lpos inz idvdl]
have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
(l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
@@ -2700,7 +2703,6 @@
assumes
linp: "islinform p"
shows "alldivide (divlcm p,p)"
-thm nz_le[OF divlcm_pos[OF linp]]
using linp divlcm_pos
proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc)
case (goal1 f)
@@ -5722,4 +5724,5 @@
use "rpresbtac.ML"
setup RPresburger.setup
*)
+
end
--- a/src/HOL/ex/SVC_Oracle.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Wed Sep 14 22:08:08 2005 +0200
@@ -3,10 +3,10 @@
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
-Installing the oracle for SVC (Stanford Validity Checker)
+Based upon the work of Søren T. Heilmann.
+*)
-Based upon the work of Søren T. Heilmann
-*)
+header {* Installing an oracle for SVC (Stanford Validity Checker) *}
theory SVC_Oracle
imports Main
--- a/src/HOL/ex/StringEx.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/StringEx.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
header {* String examples *}
--- a/src/HOL/ex/Tuple.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Tuple.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,11 +1,6 @@
(* Title: HOL/ex/Tuple.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-
-Properly nested products (see also theory Prod).
-
-Unquestionably, this should be used as the standard representation of
-tuples in HOL, but it breaks many existing theories!
*)
header {* Properly nested products *}
--- a/src/HOL/ex/svc_test.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/svc_test.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,5 +1,11 @@
-svc_test = SVC_Oracle +
+(* $Id$ *)
+
+header {* Demonstrating the interface SVC *}
+
+theory svc_test
+imports SVC_Oracle
+begin
syntax
"<->" :: [bool, bool] => bool (infixr 25)