Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added the $Id:$ line
authorpaulson
Thu, 26 Oct 2000 11:27:48 +0200
changeset 10341 6eb91805a012
parent 10340 0a380ac80e7d
child 10342 b124d59f7b61
added the $Id:$ line
doc-src/TutorialI/Inductive/Even.tex file | annotate | diff | comparison | revisions
doc-src/TutorialI/Inductive/Even.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Inductive/ROOT.ML file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/Basic.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/Blast.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/Force.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/Primes.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/ROOT.ML file | annotate | diff | comparison | revisions
doc-src/TutorialI/Rules/rules.tex file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/Examples.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/Functions.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/ROOT.ML file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/Recur.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/Relations.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Sets/sets.tex file | annotate | diff | comparison | revisions 
--- 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
--- 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
--- 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";
 
--- 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)"
--- 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))))   =    
--- 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:
 
 
--- 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:
--- 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";
--- 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}
  
--- 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"
--- 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"
--- 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";
--- 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"
--- 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"
--- 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
isabelle