# HG changeset patch
# User paulson
# Date 972552468 -7200
# Node ID 6eb91805a012c4a8bb6a839ba0f39ffd4eec7c2c
# Parent  0a380ac80e7d41676174d0e8b71b3261f11971ef
added the $Id:$ line

diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Inductive/Even.tex
--- a/doc-src/TutorialI/Inductive/Even.tex	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Even.tex	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+% ID:         $Id$
 \section{The set of even numbers}
 
 The set of even numbers can be inductively defined as the least set
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Inductive/Even.thy
--- a/doc-src/TutorialI/Inductive/Even.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Even = Main:
 
 text{*We begin with a simple example: the set of even numbers.  Obviously this
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Inductive/ROOT.ML
--- a/doc-src/TutorialI/Inductive/ROOT.ML	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Inductive/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
@@ -1,4 +1,6 @@
 use "../settings.ML";
+use_thy "Even";
 use_thy "Star";
 use_thy "AB";
+use_thy "Acc";
 
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Basic = Main:
 
 lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)"
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/Blast.thy
--- a/doc-src/TutorialI/Rules/Blast.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/Blast.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Blast = Main:
 
 lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y))))   =    
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/Force.thy
--- a/doc-src/TutorialI/Rules/Force.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Force = Main:
 
 
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 (* EXTRACT from HOL/ex/Primes.thy*)
 
 theory Primes = Main:
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/ROOT.ML
--- a/doc-src/TutorialI/Rules/ROOT.ML	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 use_thy "Basic";
 use_thy "Blast";
 use_thy "Force";
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+% ID:         $Id$
 \chapter{The Rules of the Game}
 \label{chap:rules}
  
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Examples = Main:
 
 ML "reset eta_contract"
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/Functions.thy
--- a/doc-src/TutorialI/Sets/Functions.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Functions = Main:
 
 ML "Pretty.setmargin 64"
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/ROOT.ML
--- a/doc-src/TutorialI/Sets/ROOT.ML	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 use_thy "Examples";
 use_thy "Functions";
 use_thy "Relations";
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/Recur.thy
--- a/doc-src/TutorialI/Sets/Recur.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Recur = Main:
 
 ML "Pretty.setmargin 64"
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+(* ID:         $Id$ *)
 theory Relations = Main:
 
 ML "Pretty.setmargin 64"
diff -r 0a380ac80e7d -r 6eb91805a012 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Thu Oct 26 10:27:04 2000 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Thu Oct 26 11:27:48 2000 +0200
@@ -1,3 +1,4 @@
+% ID:         $Id$
 \chapter{Sets, Functions and Relations}
 
 Mathematics relies heavily on set theory: not just unions and intersections