# HG changeset patch
# User nipkow
# Date 1025086641 -7200
# Node ID efd5db7dc7ccfcbff372f4bedcb16556f3320e5a
# Parent  4b3de63701841df832ce4e1e30fb487c5ae38d2e
*** empty log message ***

diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/FP0.thy
--- a/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -17,7 +17,6 @@
 theorem rev_rev [simp]: "rev(rev xs) = xs"
 (*<*)oops(*>*)
 
-
 text{*
 \begin{exercise}
 Define a datatype of binary trees and a function @{term mirror}
@@ -29,5 +28,4 @@
 @{prop"flatten(mirror t) = rev(flatten t)"}.
 \end{exercise}
 *}
-
 end
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/FP1.thy
--- a/doc-src/TutorialI/Overview/FP1.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP1.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,4 @@
-(*<*)
-theory FP1 = Main:
-(*>*)
+(*<*)theory FP1 = Main:(*>*)
 
 lemma "if xs = ys
        then rev xs = rev ys
@@ -28,9 +26,7 @@
 apply(auto)
 done
 
-text{*
-Some examples of linear arithmetic:
-*}
+text{*Some examples of linear arithmetic:*}
 
 lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n"
 by(auto)
@@ -38,9 +34,7 @@
 lemma "min i (max j k) = max (min k i) (min i (j::nat))"
 by(arith)
 
-text{*
-Not proved automatically because it involves multiplication:
-*}
+text{*Not proved automatically because it involves multiplication:*}
 
 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
 (*<*)oops(*>*)
@@ -75,9 +69,7 @@
 lemma fst_conv[simp]: "fst(x,y) = x"
 by auto
 
-text{*
-Setting and resetting the @{text simp} attribute:
-*}
+text{*Setting and resetting the @{text simp} attribute:*}
 
 declare fst_conv[simp]
 declare fst_conv[simp del]
@@ -94,7 +86,7 @@
 
 lemma "\<forall>x::nat. x*(y+z) = r"
 apply (simp add: add_mult_distrib2)
-(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
+(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}
 
 lemma "rev(rev(xs @ [])) = xs"
 apply (simp del: rev_rev_ident)
@@ -129,7 +121,7 @@
 
 lemma "\<forall>xs. if xs = [] then A else B"
 apply simp
-(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
+(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}
 
 lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"
 apply simp
@@ -139,15 +131,11 @@
 
 subsubsection{*Arithmetic*}
 
-text{*
-Is simple enough for the default arithmetic:
-*}
+text{*Is simple enough for the default arithmetic:*}
 lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n"
 by simp
 
-text{*
-Contains boolean combinations and needs full arithmetic:
-*}
+text{*Contains boolean combinations and needs full arithmetic:*}
 lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n"
 apply simp
 by(arith)
@@ -161,7 +149,6 @@
 (*>*)
 
 
-
 subsection{*Case Study: Compiling Expressions*}
 
 
@@ -262,7 +249,6 @@
 datatype tree = C "tree list"
 
 text{*Some trees:*}
-
 term "C []"
 term "C [C [C []], C []]"
 
@@ -287,7 +273,6 @@
 \end{exercise}
 *}
 
-
 subsubsection{*Datatypes Involving Functions*}
 
 datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
@@ -309,13 +294,9 @@
 \begin{verbatim}
 datatype lambda = C "lambda => lambda"
 \end{verbatim}
-*}
 
-text{*
 \begin{exercise}
 Define a datatype of ordinals and the ordinal $\Gamma_0$.
 \end{exercise}
 *}
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/Ind.thy
--- a/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -22,8 +22,7 @@
 subsubsection{*Rule Induction*}
 
 text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
-@{thm[display] even.induct[no_vars]}
-*}
+@{thm[display] even.induct[no_vars]}*}
 (*<*)thm even.induct[no_vars](*>*)
 
 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
@@ -83,8 +82,7 @@
 \begin{exercise}
 Show that the converse of @{thm[source]rtc_step} also holds:
 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
-\end{exercise}
-*}
+\end{exercise}*}
 
 subsection{*The accessible part of a relation*}
 
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/Ordinal.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Ordinal.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -0,0 +1,52 @@
+theory Ordinal = Main:
+
+datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
+
+consts
+  pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
+primrec
+  "pred Zero n = None"
+  "pred (Succ a) n = Some a"
+  "pred (Limit f) n = Some (f n)"
+
+constdefs
+  OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+  "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
+  OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<Squnion>")
+  "\<Squnion>f \<equiv> OpLim (power f)"
+
+consts
+  cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+  "cantor a Zero = Succ a"
+  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+
+consts
+  Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<nabla>")
+primrec
+  "\<nabla>f Zero = f Zero"
+  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+
+constdefs
+  deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+  "deriv f \<equiv> \<nabla>(\<Squnion>f)"
+
+consts
+  veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+  "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
+  "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
+  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+
+constdefs
+  veb :: "ordinal \<Rightarrow> ordinal"
+  "veb a \<equiv> veblen a Zero"
+  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
+  "\<epsilon>\<^sub>0 \<equiv> veb Zero"
+  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
+  "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
+thm Gamma0_def
+
+end
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/Rules.thy
--- a/doc-src/TutorialI/Overview/Rules.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Rules.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,4 @@
-(*<*)
-theory Rules = Main:
-(*>*)
+(*<*)theory Rules = Main:(*>*)
 
 section{*The Rules of the Game*}
 
@@ -19,9 +17,7 @@
 \end{center}
 *}
 
-(*<*)
-thm impI conjI disjI1 disjI2 iffI
-(*>*)
+(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)
 
 lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
 apply(rule impI)
@@ -45,13 +41,11 @@
 \end{tabular}
 \end{center}
 *}
-
 (*<*)
 thm impE mp
 thm conjE
 thm disjE
 (*>*)
-
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply (erule disjE)
  apply (rule disjI2)
@@ -74,9 +68,7 @@
 \end{center}
 *}
 
-(*<*)
-thm conjunct1 conjunct1 iffD1 iffD2
-(*>*)
+(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)
 
 lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
 apply (rule conjI)
@@ -100,13 +92,11 @@
 \end{tabular}
 \end{center}
 *}
-
 (*<*)
 thm allI exI
 thm allE exE
 thm spec
 (*>*)
-
 lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
 (*<*)oops(*>*)
 
@@ -160,7 +150,6 @@
 \end{tabular}
 \end{center}
 *}
-
 (*<*)
 thm append_self_conv
 thm append_self_conv[of _ "[]"]
@@ -168,7 +157,6 @@
 thm sym[OF append_self_conv]
 thm append_self_conv[THEN sym]
 (*>*)
-
 subsection{*Further Useful Methods*}
 
 lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
@@ -178,7 +166,6 @@
 done
 
 text{* And a cute example: *}
-
 lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
          \<forall>x y z. sqrt x * sqrt x = x \<and>
                   x ^ 2 = x * x \<and>
@@ -192,7 +179,6 @@
 apply simp
 done
 *)
-(*<*)
-oops
-end
-(*>*)
+(*<*)oops
+
+end(*>*)
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/Sets.thy
--- a/doc-src/TutorialI/Overview/Sets.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Sets.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,5 @@
-(*<*)
-theory Sets = Main:
-(*>*)
+(*<*)theory Sets = Main:(*>*)
+
 section{*Sets, Functions and Relations*}
 
 subsection{*Set Notation*}
@@ -13,8 +12,7 @@
 @{term "{a,b}"} & @{text "{x. P x}"} \\
 @{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
 \end{tabular}
-\end{center}
-*}
+\end{center}*}
 (*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
 term "a \<in> A" term "b \<notin> A"
 term "{a,b}" term "{x. P x}"
@@ -28,8 +26,7 @@
 @{thm o_def[no_vars]}\\
 @{thm image_def[no_vars]}\\
 @{thm vimage_def[no_vars]}
-\end{tabular}
-*}
+\end{tabular}*}
 (*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
 
 subsection{*Some Relations*}
@@ -42,16 +39,13 @@
 @{thm rtrancl_refl[no_vars]}\\
 @{thm rtrancl_into_rtrancl[no_vars]}\\
 @{thm trancl_def[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm Id_def
+\end{tabular}*}
+(*<*)thm Id_def
 thm converse_def[no_vars]
 thm Image_def[no_vars]
 thm relpow.simps[no_vars]
 thm rtrancl.intros[no_vars]
-thm trancl_def[no_vars]
-(*>*)
+thm trancl_def[no_vars](*>*)
 
 subsection{*Wellfoundedness*}
 
@@ -59,12 +53,9 @@
 \begin{tabular}{l}
 @{thm wf_def[no_vars]}\\
 @{thm wf_iff_no_infinite_down_chain[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm wf_def[no_vars]
-thm wf_iff_no_infinite_down_chain[no_vars]
-(*>*)
+\end{tabular}*}
+(*<*)thm wf_def[no_vars]
+thm wf_iff_no_infinite_down_chain[no_vars](*>*)
 
 subsection{*Fixed Point Operators*}
 
@@ -73,13 +64,10 @@
 @{thm lfp_def[no_vars]}\\
 @{thm lfp_unfold[no_vars]}\\
 @{thm lfp_induct[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm lfp_def gfp_def
+\end{tabular}*}
+(*<*)thm lfp_def gfp_def
 thm lfp_unfold
-thm lfp_induct
-(*>*)
+thm lfp_induct(*>*)
 
 subsection{*Case Study: Verified Model Checking*}
 
@@ -151,8 +139,5 @@
 
 Show that the semantics for @{term EF} satisfies the following recursion equation:
 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
-\end{exercise}
-*}
-(*<*)
-end
-(*>*)
+\end{exercise}*}
+(*<*)end(*>*)
diff -r 4b3de6370184 -r efd5db7dc7cc doc-src/TutorialI/Overview/delete-verbatim
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/delete-verbatim	Wed Jun 26 12:17:21 2002 +0200
@@ -0,0 +1,34 @@
+#!/usr/bin/perl -w
+
+sub doit {
+    my ($file) = @_;
+
+    open (FILE, $file) || die $!;
+    undef $/; $text = <FILE>; $/ = "\n";
+    close FILE || die $!;
+
+    $_ = $text;
+
+    s/text_raw\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
+    s/text\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
+    s/\(\*<\*\)//sg;
+    s/\(\*>\*\)//sg;
+
+    $result = $_;
+
+    if ($text ne $result) {
+        print STDERR "fixing $file\n";
+#        if (! -f "$file~~") {
+#            rename $file, "$file~~" || die $!;
+#        }
+        open (FILE, "> Demo/$file") || die $!;
+        print FILE $result;
+        close FILE || die $!;
+    }
+}
+
+
+foreach $file (@ARGV) {
+  eval { &doit($file); };
+  if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
+}