# HG changeset patch
# User nipkow
# Date 971368703 -7200
# Node ID 33fe2d701ddda1b8f09cdddfd0397e9480a5730b
# Parent  1bece7f35762fd65f466bc1271a2b85fc5d4ec35
*** empty log message ***

diff -r 1bece7f35762 -r 33fe2d701ddd TFL/rules.sml
--- a/TFL/rules.sml	Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/rules.sml	Thu Oct 12 18:38:23 2000 +0200
@@ -482,7 +482,7 @@
   let val {prop, ...} = rep_thm thm
   in case prop 
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
       | _ => true
   end;
 
@@ -685,7 +685,7 @@
   end;
 
 fun restricted t = is_some (S.find_term
-			    (fn (Const("WF.cut",_)) =>true | _ => false) 
+			    (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false) 
 			    t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r 1bece7f35762 -r 33fe2d701ddd TFL/thms.sml
--- a/TFL/thms.sml	Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/thms.sml	Thu Oct 12 18:38:23 2000 +0200
@@ -17,9 +17,9 @@
 
 structure Thms: Thms_sig =
 struct
-   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
-   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
-   val CUT_DEF = get_thm WF.thy "cut_def";
+   val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
+   val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
+   val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
 
    val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
      (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
diff -r 1bece7f35762 -r 33fe2d701ddd TFL/usyntax.sml
--- a/TFL/usyntax.sml	Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/usyntax.sml	Thu Oct 12 18:38:23 2000 +0200
@@ -407,7 +407,7 @@
                                   mesg="unexpected term structure"} (* FIXME do not handle _ !!! *)
    else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
 
-fun is_WFR (Const("WF.wf",_)$_) = true
+fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -2,7 +2,7 @@
 
 subsection{*Computation tree logic---CTL*};
 
-text{*
+text{*\label{sec:CTL}
 The semantics of PDL only needs transitive reflexive closure.
 Let us now be a bit more adventurous and introduce a new temporal operator
 that goes beyond transitive reflexive closure. We extend the datatype
@@ -266,16 +266,20 @@
  apply(fast intro:someI2_ex);
 
 txt{*\noindent
-What is worth noting here is that we have used @{text fast} rather than @{text blast}.
-The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}:
-unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
-variables. For efficiency reasons @{text blast} does not even attempt such unifications.
-Although @{text fast} can in principle cope with complicated unification problems, in practice
-the number of unifiers arising is often prohibitive and the offending rule may need to be applied
-explicitly rather than automatically.
+What is worth noting here is that we have used @{text fast} rather than
+@{text blast}.  The reason is that @{text blast} would fail because it cannot
+cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
+subgoal is nontrivial because of the nested schematic variables. For
+efficiency reasons @{text blast} does not even attempt such unifications.
+Although @{text fast} can in principle cope with complicated unification
+problems, in practice the number of unifiers arising is often prohibitive and
+the offending rule may need to be applied explicitly rather than
+automatically. This is what happens in the step case.
 
-The induction step is similar, but more involved, because now we face nested occurrences of
-@{text SOME}. We merely show the proof commands but do not describe th details:
+The induction step is similar, but more involved, because now we face nested
+occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
+solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
+show the proof commands but do not describe the details:
 *};
 
 apply(simp);
@@ -397,53 +401,4 @@
 a fixpoint is reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.
 *}
-
-(*<*)
-(*
-Second proof of opposite direction, directly by wellfounded induction
-on the initial segment of M that avoids A.
-
-Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
-*)
-
-consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
-inductive "Avoid s A"
-intros "s \<in> Avoid s A"
-       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
-
-(* For any infinite A-avoiding path (f) in Avoid s A,
-   there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
-*)
-lemma ex_infinite_path[rule_format]:
-"t \<in> Avoid s A  \<Longrightarrow>
- \<forall>f. t = f 0 \<longrightarrow> (\<forall>i. (f i, f (Suc i)) \<in> M \<and> f i \<in> Avoid s A \<and> f i \<notin> A)
-                \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
-apply(simp add:Paths_def);
-apply(erule Avoid.induct);
- apply(blast);
-apply(rule allI);
-apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
-by(force split:nat.split);
-
-lemma Avoid_in_lfp[rule_format(no_asm)]:
-"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
-apply(subgoal_tac "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
- apply(erule_tac a = t in wf_induct);
- apply(clarsimp);
- apply(rule ssubst [OF lfp_unfold[OF mono_af]]);
- apply(unfold af_def);
- apply(blast intro:Avoid.intros);
-apply(erule contrapos2);
-apply(simp add:wf_iff_no_infinite_down_chain);
-apply(erule exE);
-apply(rule ex_infinite_path);
-by(auto);
-
-theorem AF_lemma2:
-"{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
-apply(rule subsetI);
-apply(simp);
-apply(erule Avoid_in_lfp);
-by(rule Avoid.intros);
-
-end(*>*)
+(*<*)end(*>*)
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -118,11 +118,10 @@
 \ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
 \end{isabelle}
-which is proved by @{text blast} with the help of a few lemmas about
-@{text"^*"}:
+which is proved by @{text blast} with the help of transitivity of @{text"^*"}:
 *}
 
- apply(blast intro: r_into_rtrancl rtrancl_trans);
+ apply(blast intro: rtrancl_trans);
 
 txt{*
 We now return to the second set containment subgoal, which is again proved
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/CTL/ROOT.ML
--- a/doc-src/TutorialI/CTL/ROOT.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/ROOT.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -1,3 +1,4 @@
 use "../settings.ML";
 use_thy "PDL";
 use_thy "CTL";
+use_thy "CTLind";
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:38:23 2000 +0200
@@ -197,16 +197,20 @@
 \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
-The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
-unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
-variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
-Although \isa{fast} can in principle cope with complicated unification problems, in practice
-the number of unifiers arising is often prohibitive and the offending rule may need to be applied
-explicitly rather than automatically.
+What is worth noting here is that we have used \isa{fast} rather than
+\isa{blast}.  The reason is that \isa{blast} would fail because it cannot
+cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
+subgoal is nontrivial because of the nested schematic variables. For
+efficiency reasons \isa{blast} does not even attempt such unifications.
+Although \isa{fast} can in principle cope with complicated unification
+problems, in practice the number of unifiers arising is often prohibitive and
+the offending rule may need to be applied explicitly rather than
+automatically. This is what happens in the step case.
 
-The induction step is similar, but more involved, because now we face nested occurrences of
-\isa{SOME}. We merely show the proof commands but do not describe th details:%
+The induction step is similar, but more involved, because now we face nested
+occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
+solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely
+show the proof commands but do not describe the details:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:38:23 2000 +0200
@@ -113,10 +113,9 @@
 \ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
 \end{isabelle}
-which is proved by \isa{blast} with the help of a few lemmas about
-\isa{{\isacharcircum}{\isacharasterisk}}:%
+which is proved by \isa{blast} with the help of transitivity of \isa{{\isacharcircum}{\isacharasterisk}}:%
 \end{isamarkuptxt}%
-\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ r{\isacharunderscore}into{\isacharunderscore}rtrancl\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
+\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptxt}%
 We now return to the second set containment subgoal, which is again proved
 pointwise:%
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu Oct 12 18:38:23 2000 +0200
@@ -106,7 +106,7 @@
 
 HOL-CTL: HOL $(LOG)/HOL-CTL.gz
 
-$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
+$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
 	@rm -f tutorial.dvi
 
@@ -126,4 +126,4 @@
 ## clean
 
 clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz 
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -66,10 +66,9 @@
 @{thm[display,margin=50]"map_cong"[no_vars]}
 Its second premise expresses (indirectly) that the second argument of
 @{term"map"} is only applied to elements of its third argument. Congruence
-rules for other higher-order functions on lists would look very similar but
-have not been proved yet because they were never needed. If you get into a
-situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append a hint locally
+rules for other higher-order functions on lists look very similar. If you get
+into a situation where you need to supply \isacommand{recdef} with new
+congruence rules, you can either append a hint locally
 to the specific occurrence of \isacommand{recdef}
 *}
 (*<*)
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Thu Oct 12 18:38:23 2000 +0200
@@ -66,10 +66,9 @@
 \end{isabelle}
 Its second premise expresses (indirectly) that the second argument of
 \isa{map} is only applied to elements of its third argument. Congruence
-rules for other higher-order functions on lists would look very similar but
-have not been proved yet because they were never needed. If you get into a
-situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append a hint locally
+rules for other higher-order functions on lists look very similar. If you get
+into a situation where you need to supply \isacommand{recdef} with new
+congruence rules, you can either append a hint locally
 to the specific occurrence of \isacommand{recdef}%
 \end{isamarkuptext}%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Thu Oct 12 18:38:23 2000 +0200
@@ -15,8 +15,6 @@
 
 swap in classical.ML has ugly name Pa in it. Rename.
 
-list of ^*/^+ intro rules. Incl transitivity?
-
 Induction rules for int: int_le/ge_induct?
 Needed for ifak example. But is that example worth it?
 
diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Thu Oct 12 18:38:23 2000 +0200
@@ -67,7 +67,7 @@
 \input{fp}
 \chapter{The Rules of the Game}
 \input{sets}
-\chapter{Inductively Defined Sets}
+\input{Inductive/inductive}
 \input{Advanced/advanced}
 \chapter{More about Types}
 \chapter{Theory Presentation}
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Datatype.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1998  TU Muenchen
 *)
 
-Datatype = Univ +
+Datatype = Datatype_Universe +
 
 rep_datatype bool
   distinct True_not_False, False_not_True
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Divides.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 The division operators div, mod and the divides relation "dvd"
 *)
 
-Divides = Arith +
+Divides = Arithmetic +
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 Notions about functions.
 *)
 
-Fun = Vimage + equalities + 
+Fun = Inverse_Image + equalities + 
 
 instance set :: (term) order
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/IOA/Asig.thy
--- a/src/HOL/IOA/Asig.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/IOA/Asig.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 Action signatures
 *)
 
-Asig = Prod +
+Asig = Product_Type +
 
 types 
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/Comb.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -65,12 +65,12 @@
 
 Goal "x ---> y ==> x#z ---> y#z";
 by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
 qed "Ap_reduce1";
 
 Goal "x ---> y ==> z#x ---> z#y";
 by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/LList.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -782,7 +782,7 @@
 by (ALLGOALS Asm_simp_tac);
 qed "fun_power_Suc";
 
-val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
+val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
  [("f","Pair")] (standard(refl RS cong RS cong));
 
 (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/Sexp.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
 structures by hand.
 *)
 
-Sexp = Univ + Inductive +
+Sexp = Datatype_Universe + Inductive +
 consts
   sexp      :: 'a item set
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Inductive.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
 *)
 
-theory Inductive = Gfp + Prod + Sum + NatDef
+theory Inductive = Gfp + Sum_Type + NatDef
 files
   "Tools/induct_method.ML"
   "Tools/inductive_package.ML"
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 The integers as equivalence classes over nat*nat.
 *)
 
-IntDef = Equiv + Arith +
+IntDef = Equiv + Arithmetic +
 constdefs
   intrel      :: "((nat * nat) * (nat * nat)) set"
   "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/IsaMakefile	Thu Oct 12 18:38:23 2000 +0200
@@ -69,7 +69,7 @@
   $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
   $(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
   $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
-  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \
+  Arithmetic.ML Arithmetic.thy Calculation.thy Datatype.thy Divides.ML \
   Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
   HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
   Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
@@ -80,17 +80,17 @@
   Integ/int_arith2.ML Integ/nat_simprocs.ML Lfp.ML Lfp.thy List.ML \
   List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
   NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
-  Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy \
-  RelPow.ML RelPow.thy Relation.ML Relation.thy Set.ML Set.thy \
+  Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+  Relation_Power.ML Relation_Power.thy Relation.ML Relation.thy Set.ML Set.thy \
   SetInterval.ML SetInterval.thy String.thy SVC_Oracle.ML \
-  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
+  SVC_Oracle.thy Sum_Type.ML Sum_Type.thy Tools/datatype_aux.ML \
   Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   Tools/induct_method.ML Tools/inductive_package.ML Tools/meson.ML \
   Tools/numeral_syntax.ML Tools/primrec_package.ML \
   Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
-  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy While.ML \
+  Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy Datatype_Universe.ML Datatype_Universe.thy \
+  Inverse_Image.ML Inverse_Image.thy Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML Wellfounded_Relations.thy While.ML \
   While.thy arith_data.ML blastdata.ML cladata.ML equalities.ML \
   equalities.thy hologic.ML meson_lemmas.ML mono.ML mono.thy simpdata.ML \
   subset.ML subset.thy thy_syntax.ML
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -132,7 +132,7 @@
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
   apply (erule rtrancl_induct)
    apply blast
-  apply (blast del: rtrancl_refl intro: rtranclIs)
+  apply (blast del: rtrancl_refl intro: rtrancl_trans)
   done
 
 end
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Lfp.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = mono + Prod +
+Lfp = mono + Product_Type +
 
 constdefs
   lfp :: ['a set=>'a set] => 'a set
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -13,19 +13,19 @@
 
 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
 
-val select_split = prove_goalw Prod.thy [split_def] 
+val select_split = prove_goalw Product_Type.thy [split_def] 
 	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
 	 
 
-val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
+val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
 	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
-val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
+val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
 	(fn _ => [Auto_tac]);
-val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
+val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
 	rtac (split_beta RS subst) 1,
 	rtac (hd prems) 1]);
-val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
+val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
 	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
 	rtac (hd prems) 1]);
@@ -131,11 +131,11 @@
 by(simp_tac (simpset() addsimps image_def::premises()) 1);
 qed "image_cong";
 
-val split_Pair_eq = prove_goal Prod.thy 
+val split_Pair_eq = prove_goal Product_Type.thy 
 "!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
 	etac imageE 1,
 	split_all_tac 1,
-	auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
+	auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
 
 
 (* More about Maps *)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -147,7 +147,7 @@
 
 (* first simplification, then model checking *)
 
-goalw Prod.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+goalw Product_Type.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   by (rtac ext 1);
   by (stac (surjective_pairing RS sym) 1);
   by (rtac refl 1);
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/NatDef.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -8,7 +8,7 @@
 Type nat is defined as a set Nat over type ind.
 *)
 
-NatDef = WF +
+NatDef = Wellfounded_Recursion +
 
 (** type ind **)
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/PreList.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -8,8 +8,8 @@
 *)
 
 theory PreList =
-  Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
-  SVC_Oracle + While:
+  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
+  Relation_Power + Calculation + SVC_Oracle + While:
 
 theorems [cases type: bool] = case_split
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -94,9 +94,9 @@
     [real_minus_add_distrib]));
 qed "sumr_minus";
 
-context Arith.thy;
+context Arithmetic.thy;
 
-goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
+Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
 by (auto_tac (claset() addSDs [not_leE],simpset()));
 qed "lemma_not_Suc_add";
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Recdef.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -5,7 +5,7 @@
 TFL: recursive function definitions.
 *)
 
-theory Recdef = WF_Rel + Datatype
+theory Recdef = Wellfounded_Relations + Datatype
 files
   "../TFL/utils.sml"
   "../TFL/usyntax.sml"
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1996  University of Cambridge
 *)
 
-Relation = Prod +
+Relation = Product_Type +
 
 constdefs
   converse :: "('a*'b) set => ('b*'a) set"               ("(_^-1)" [1000] 999)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/SetInterval.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 lessThan, greaterThan, atLeast, atMost
 *)
 
-SetInterval = equalities + Arith + 
+SetInterval = equalities + Arithmetic + 
 
 constdefs
  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -417,7 +417,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -715,7 +715,7 @@
     val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       [descr] sorts thy7;
     val (thy9, size_thms) =
-      if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
+      if exists (equal "Arithmetic") (Sign.stamp_names_of (Theory.sign_of thy8)) then
         DatatypeAbsProofs.prove_size_thms false new_type_names
           [descr] sorts reccomb_names rec_thms thy8
       else (thy8, []);
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -398,7 +398,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
 
-    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
         (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -185,7 +185,7 @@
 
 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
 
-val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "vimage";
+val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage";
 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
 
 (* make injections needed in mutually recursive definitions *)
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/UNITY/Reach.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -31,7 +31,7 @@
 
 Goal "Rprg : Always reach_invariant";
 by (always_tac 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
 qed "reach_invariant";
 
 
@@ -42,7 +42,7 @@
      "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
 by (rtac equalityI 1);
 by (auto_tac (claset() addSIs [ext], simpset()));
-by (blast_tac (claset() addIs rtranclIs) 2);
+by (blast_tac (claset() addIs [rtrancl_trans]) 2);
 by (etac rtrancl_induct 1);
 by Auto_tac;
 qed "fixedpoint_invariant_correct";
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/ex/PiSets.thy
--- a/src/HOL/ex/PiSets.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/PiSets.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
 Also the nice -> operator for function space
 *)
 
-PiSets = Univ + Finite +
+PiSets = Datatype_Universe + Finite +
 
 syntax
   "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/cla.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -462,7 +462,7 @@
 
 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   Fast_tac indeed copes!*)
-goal Prod.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
 \             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
 \             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
 by (Fast_tac 1);
@@ -470,7 +470,7 @@
 
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   It does seem obvious!*)
-goal Prod.thy
+goal Product_Type.thy
     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
@@ -488,7 +488,7 @@
 by (Blast_tac 1);
 result();
 
-goal Prod.thy
+goal Product_Type.thy
     "(ALL x y. R(x,y) | R(y,x)) &                \
 \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
 \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/mesontest2.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -11,9 +11,9 @@
 (*All but the fastest are ignored to reduce build time*)
 val even_hard_ones = false;
 
-(*Prod.thy instead of HOL.thy regards arguments as tuples.
+(*Product_Type.thy instead of HOL.thy regards arguments as tuples.
   But Main.thy would allow clashes with many other constants*)
-fun prove (s,tac) = prove_goal Prod.thy s (fn [] => [tac]);
+fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
 
 fun prove_hard arg = if even_hard_ones then prove arg else TrueI;
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/Cprod1.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -3,7 +3,7 @@
     Author:     Franz Regensburger
     Copyright   1993  Technische Universitaet Muenchen
 
-Partial ordering for cartesian product of HOL theory Prod.thy
+Partial ordering for cartesian product of HOL theory Product_Type.thy
 *)
 
 
@@ -15,7 +15,7 @@
 by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
-by (asm_simp_tac (simpset_of Prod.thy) 1);
+by (asm_simp_tac (simpset_of Product_Type.thy) 1);
 qed "Sel_injective_cprod";
 
 Goalw [less_cprod_def] "(p::'a*'b) << p";
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/ABP/Lemmas.thy
--- a/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,4 +6,4 @@
 Arithmetic lemmas
 *)
 
-Lemmas = Arith
+Lemmas = Arithmetic
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOLCF/IOA/ABP/Packet.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Packet.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 Packets
 *)
 
-Packet = Arith +
+Packet = Arithmetic +
 
 types
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Oct 12 18:38:23 2000 +0200
@@ -35,7 +35,7 @@
 
 (* Arithmetic *)
 
-goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
+goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
 qed "pred_suc";
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/NTP/Lemmas.thy
--- a/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,4 +6,4 @@
 Arithmetic lemmas
 *)
 
-Lemmas = Arith
+Lemmas = Arithmetic
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOLCF/IOA/NTP/Multiset.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
 Should be done as a subtype and moved to a global place.
 *)
 
-Multiset = Arith + Lemmas +
+Multiset = Lemmas +
 
 types
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/IOA/NTP/Packet.thy
--- a/src/HOLCF/IOA/NTP/Packet.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
 Packets
 *)
 
-Packet = Arith + Multiset +  
+Packet = Multiset +  
 
 types
 
diff -r 1bece7f35762 -r 33fe2d701ddd src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/Up1.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -8,7 +8,7 @@
 
 *)
 
-Up1 = Cfun3 + Sum + Datatype +
+Up1 = Cfun3 + Sum_Type + Datatype +
 
 (* new type for lifting *)