*** empty log message ***
authornipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 1021233fe2d701ddd
parent 10211 1bece7f35762
child 10213 01c2744a3786
*** empty log message ***
TFL/rules.sml
TFL/thms.sml
TFL/usyntax.sml
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/ROOT.ML
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Fun.thy
src/HOL/IOA/Asig.thy
src/HOL/Induct/Comb.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Sexp.thy
src/HOL/Inductive.thy
src/HOL/Integ/IntDef.thy
src/HOL/IsaMakefile
src/HOL/Lambda/Commutation.thy
src/HOL/Lfp.thy
src/HOL/MicroJava/J/JBasis.ML
src/HOL/Modelcheck/MuckeSyn.ML
src/HOL/NatDef.thy
src/HOL/PreList.thy
src/HOL/Real/Hyperreal/Series.ML
src/HOL/Recdef.thy
src/HOL/Relation.thy
src/HOL/SetInterval.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/inductive_package.ML
src/HOL/UNITY/Reach.ML
src/HOL/ex/PiSets.thy
src/HOL/ex/cla.ML
src/HOL/ex/mesontest2.ML
src/HOLCF/Cprod1.ML
src/HOLCF/IOA/ABP/Lemmas.thy
src/HOLCF/IOA/ABP/Packet.thy
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/NTP/Lemmas.thy
src/HOLCF/IOA/NTP/Multiset.thy
src/HOLCF/IOA/NTP/Packet.thy
src/HOLCF/Up1.thy
     1.1 --- a/TFL/rules.sml	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/TFL/rules.sml	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -482,7 +482,7 @@
     1.4    let val {prop, ...} = rep_thm thm
     1.5    in case prop 
     1.6       of (Const("==>",_)$(Const("Trueprop",_)$ _) $
     1.7 -         (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
     1.8 +         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
     1.9        | _ => true
    1.10    end;
    1.11  
    1.12 @@ -685,7 +685,7 @@
    1.13    end;
    1.14  
    1.15  fun restricted t = is_some (S.find_term
    1.16 -			    (fn (Const("WF.cut",_)) =>true | _ => false) 
    1.17 +			    (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false) 
    1.18  			    t)
    1.19  
    1.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
     2.1 --- a/TFL/thms.sml	Thu Oct 12 18:09:06 2000 +0200
     2.2 +++ b/TFL/thms.sml	Thu Oct 12 18:38:23 2000 +0200
     2.3 @@ -17,9 +17,9 @@
     2.4  
     2.5  structure Thms: Thms_sig =
     2.6  struct
     2.7 -   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
     2.8 -   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
     2.9 -   val CUT_DEF = get_thm WF.thy "cut_def";
    2.10 +   val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
    2.11 +   val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
    2.12 +   val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
    2.13  
    2.14     val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
    2.15       (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
     3.1 --- a/TFL/usyntax.sml	Thu Oct 12 18:09:06 2000 +0200
     3.2 +++ b/TFL/usyntax.sml	Thu Oct 12 18:38:23 2000 +0200
     3.3 @@ -407,7 +407,7 @@
     3.4                                    mesg="unexpected term structure"} (* FIXME do not handle _ !!! *)
     3.5     else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
     3.6  
     3.7 -fun is_WFR (Const("WF.wf",_)$_) = true
     3.8 +fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
     3.9    | is_WFR _                 = false;
    3.10  
    3.11  fun ARB ty = mk_select{Bvar=Free("v",ty),
     4.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Thu Oct 12 18:09:06 2000 +0200
     4.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Oct 12 18:38:23 2000 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4  
     4.5  subsection{*Computation tree logic---CTL*};
     4.6  
     4.7 -text{*
     4.8 +text{*\label{sec:CTL}
     4.9  The semantics of PDL only needs transitive reflexive closure.
    4.10  Let us now be a bit more adventurous and introduce a new temporal operator
    4.11  that goes beyond transitive reflexive closure. We extend the datatype
    4.12 @@ -266,16 +266,20 @@
    4.13   apply(fast intro:someI2_ex);
    4.14  
    4.15  txt{*\noindent
    4.16 -What is worth noting here is that we have used @{text fast} rather than @{text blast}.
    4.17 -The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}:
    4.18 -unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
    4.19 -variables. For efficiency reasons @{text blast} does not even attempt such unifications.
    4.20 -Although @{text fast} can in principle cope with complicated unification problems, in practice
    4.21 -the number of unifiers arising is often prohibitive and the offending rule may need to be applied
    4.22 -explicitly rather than automatically.
    4.23 +What is worth noting here is that we have used @{text fast} rather than
    4.24 +@{text blast}.  The reason is that @{text blast} would fail because it cannot
    4.25 +cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
    4.26 +subgoal is nontrivial because of the nested schematic variables. For
    4.27 +efficiency reasons @{text blast} does not even attempt such unifications.
    4.28 +Although @{text fast} can in principle cope with complicated unification
    4.29 +problems, in practice the number of unifiers arising is often prohibitive and
    4.30 +the offending rule may need to be applied explicitly rather than
    4.31 +automatically. This is what happens in the step case.
    4.32  
    4.33 -The induction step is similar, but more involved, because now we face nested occurrences of
    4.34 -@{text SOME}. We merely show the proof commands but do not describe th details:
    4.35 +The induction step is similar, but more involved, because now we face nested
    4.36 +occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
    4.37 +solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
    4.38 +show the proof commands but do not describe the details:
    4.39  *};
    4.40  
    4.41  apply(simp);
    4.42 @@ -397,53 +401,4 @@
    4.43  a fixpoint is reached. It is actually possible to generate executable functional programs
    4.44  from HOL definitions, but that is beyond the scope of the tutorial.
    4.45  *}
    4.46 -
    4.47 -(*<*)
    4.48 -(*
    4.49 -Second proof of opposite direction, directly by wellfounded induction
    4.50 -on the initial segment of M that avoids A.
    4.51 -
    4.52 -Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
    4.53 -*)
    4.54 -
    4.55 -consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
    4.56 -inductive "Avoid s A"
    4.57 -intros "s \<in> Avoid s A"
    4.58 -       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
    4.59 -
    4.60 -(* For any infinite A-avoiding path (f) in Avoid s A,
    4.61 -   there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
    4.62 -*)
    4.63 -lemma ex_infinite_path[rule_format]:
    4.64 -"t \<in> Avoid s A  \<Longrightarrow>
    4.65 - \<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)
    4.66 -                \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
    4.67 -apply(simp add:Paths_def);
    4.68 -apply(erule Avoid.induct);
    4.69 - apply(blast);
    4.70 -apply(rule allI);
    4.71 -apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
    4.72 -by(force split:nat.split);
    4.73 -
    4.74 -lemma Avoid_in_lfp[rule_format(no_asm)]:
    4.75 -"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
    4.76 -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}");
    4.77 - apply(erule_tac a = t in wf_induct);
    4.78 - apply(clarsimp);
    4.79 - apply(rule ssubst [OF lfp_unfold[OF mono_af]]);
    4.80 - apply(unfold af_def);
    4.81 - apply(blast intro:Avoid.intros);
    4.82 -apply(erule contrapos2);
    4.83 -apply(simp add:wf_iff_no_infinite_down_chain);
    4.84 -apply(erule exE);
    4.85 -apply(rule ex_infinite_path);
    4.86 -by(auto);
    4.87 -
    4.88 -theorem AF_lemma2:
    4.89 -"{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
    4.90 -apply(rule subsetI);
    4.91 -apply(simp);
    4.92 -apply(erule Avoid_in_lfp);
    4.93 -by(rule Avoid.intros);
    4.94 -
    4.95 -end(*>*)
    4.96 +(*<*)end(*>*)
     5.1 --- a/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:09:06 2000 +0200
     5.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Oct 12 18:38:23 2000 +0200
     5.3 @@ -118,11 +118,10 @@
     5.4  \ \ \ \ \ \ \ \ \ 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
     5.5  \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
     5.6  \end{isabelle}
     5.7 -which is proved by @{text blast} with the help of a few lemmas about
     5.8 -@{text"^*"}:
     5.9 +which is proved by @{text blast} with the help of transitivity of @{text"^*"}:
    5.10  *}
    5.11  
    5.12 - apply(blast intro: r_into_rtrancl rtrancl_trans);
    5.13 + apply(blast intro: rtrancl_trans);
    5.14  
    5.15  txt{*
    5.16  We now return to the second set containment subgoal, which is again proved
     6.1 --- a/doc-src/TutorialI/CTL/ROOT.ML	Thu Oct 12 18:09:06 2000 +0200
     6.2 +++ b/doc-src/TutorialI/CTL/ROOT.ML	Thu Oct 12 18:38:23 2000 +0200
     6.3 @@ -1,3 +1,4 @@
     6.4  use "../settings.ML";
     6.5  use_thy "PDL";
     6.6  use_thy "CTL";
     6.7 +use_thy "CTLind";
     7.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:09:06 2000 +0200
     7.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 12 18:38:23 2000 +0200
     7.3 @@ -197,16 +197,20 @@
     7.4  \ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
     7.5  \begin{isamarkuptxt}%
     7.6  \noindent
     7.7 -What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
     7.8 -The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
     7.9 -unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
    7.10 -variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
    7.11 -Although \isa{fast} can in principle cope with complicated unification problems, in practice
    7.12 -the number of unifiers arising is often prohibitive and the offending rule may need to be applied
    7.13 -explicitly rather than automatically.
    7.14 +What is worth noting here is that we have used \isa{fast} rather than
    7.15 +\isa{blast}.  The reason is that \isa{blast} would fail because it cannot
    7.16 +cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
    7.17 +subgoal is nontrivial because of the nested schematic variables. For
    7.18 +efficiency reasons \isa{blast} does not even attempt such unifications.
    7.19 +Although \isa{fast} can in principle cope with complicated unification
    7.20 +problems, in practice the number of unifiers arising is often prohibitive and
    7.21 +the offending rule may need to be applied explicitly rather than
    7.22 +automatically. This is what happens in the step case.
    7.23  
    7.24 -The induction step is similar, but more involved, because now we face nested occurrences of
    7.25 -\isa{SOME}. We merely show the proof commands but do not describe th details:%
    7.26 +The induction step is similar, but more involved, because now we face nested
    7.27 +occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
    7.28 +solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely
    7.29 +show the proof commands but do not describe the details:%
    7.30  \end{isamarkuptxt}%
    7.31  \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    7.32  \isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
     8.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:09:06 2000 +0200
     8.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Thu Oct 12 18:38:23 2000 +0200
     8.3 @@ -113,10 +113,9 @@
     8.4  \ \ \ \ \ \ \ \ \ 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
     8.5  \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
     8.6  \end{isabelle}
     8.7 -which is proved by \isa{blast} with the help of a few lemmas about
     8.8 -\isa{{\isacharcircum}{\isacharasterisk}}:%
     8.9 +which is proved by \isa{blast} with the help of transitivity of \isa{{\isacharcircum}{\isacharasterisk}}:%
    8.10  \end{isamarkuptxt}%
    8.11 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ r{\isacharunderscore}into{\isacharunderscore}rtrancl\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
    8.12 +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
    8.13  \begin{isamarkuptxt}%
    8.14  We now return to the second set containment subgoal, which is again proved
    8.15  pointwise:%
     9.1 --- a/doc-src/TutorialI/IsaMakefile	Thu Oct 12 18:09:06 2000 +0200
     9.2 +++ b/doc-src/TutorialI/IsaMakefile	Thu Oct 12 18:38:23 2000 +0200
     9.3 @@ -106,7 +106,7 @@
     9.4  
     9.5  HOL-CTL: HOL $(LOG)/HOL-CTL.gz
     9.6  
     9.7 -$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
     9.8 +$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
     9.9  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
    9.10  	@rm -f tutorial.dvi
    9.11  
    9.12 @@ -126,4 +126,4 @@
    9.13  ## clean
    9.14  
    9.15  clean:
    9.16 -	@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 
    9.17 +	@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
    10.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:09:06 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:38:23 2000 +0200
    10.3 @@ -66,10 +66,9 @@
    10.4  @{thm[display,margin=50]"map_cong"[no_vars]}
    10.5  Its second premise expresses (indirectly) that the second argument of
    10.6  @{term"map"} is only applied to elements of its third argument. Congruence
    10.7 -rules for other higher-order functions on lists would look very similar but
    10.8 -have not been proved yet because they were never needed. If you get into a
    10.9 -situation where you need to supply \isacommand{recdef} with new congruence
   10.10 -rules, you can either append a hint locally
   10.11 +rules for other higher-order functions on lists look very similar. If you get
   10.12 +into a situation where you need to supply \isacommand{recdef} with new
   10.13 +congruence rules, you can either append a hint locally
   10.14  to the specific occurrence of \isacommand{recdef}
   10.15  *}
   10.16  (*<*)
    11.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Thu Oct 12 18:09:06 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Thu Oct 12 18:38:23 2000 +0200
    11.3 @@ -66,10 +66,9 @@
    11.4  \end{isabelle}
    11.5  Its second premise expresses (indirectly) that the second argument of
    11.6  \isa{map} is only applied to elements of its third argument. Congruence
    11.7 -rules for other higher-order functions on lists would look very similar but
    11.8 -have not been proved yet because they were never needed. If you get into a
    11.9 -situation where you need to supply \isacommand{recdef} with new congruence
   11.10 -rules, you can either append a hint locally
   11.11 +rules for other higher-order functions on lists look very similar. If you get
   11.12 +into a situation where you need to supply \isacommand{recdef} with new
   11.13 +congruence rules, you can either append a hint locally
   11.14  to the specific occurrence of \isacommand{recdef}%
   11.15  \end{isamarkuptext}%
   11.16  {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
    12.1 --- a/doc-src/TutorialI/todo.tobias	Thu Oct 12 18:09:06 2000 +0200
    12.2 +++ b/doc-src/TutorialI/todo.tobias	Thu Oct 12 18:38:23 2000 +0200
    12.3 @@ -15,8 +15,6 @@
    12.4  
    12.5  swap in classical.ML has ugly name Pa in it. Rename.
    12.6  
    12.7 -list of ^*/^+ intro rules. Incl transitivity?
    12.8 -
    12.9  Induction rules for int: int_le/ge_induct?
   12.10  Needed for ifak example. But is that example worth it?
   12.11  
    13.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Oct 12 18:09:06 2000 +0200
    13.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Oct 12 18:38:23 2000 +0200
    13.3 @@ -67,7 +67,7 @@
    13.4  \input{fp}
    13.5  \chapter{The Rules of the Game}
    13.6  \input{sets}
    13.7 -\chapter{Inductively Defined Sets}
    13.8 +\input{Inductive/inductive}
    13.9  \input{Advanced/advanced}
   13.10  \chapter{More about Types}
   13.11  \chapter{Theory Presentation}
    14.1 --- a/src/HOL/Datatype.thy	Thu Oct 12 18:09:06 2000 +0200
    14.2 +++ b/src/HOL/Datatype.thy	Thu Oct 12 18:38:23 2000 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4      Copyright   1998  TU Muenchen
    14.5  *)
    14.6  
    14.7 -Datatype = Univ +
    14.8 +Datatype = Datatype_Universe +
    14.9  
   14.10  rep_datatype bool
   14.11    distinct True_not_False, False_not_True
    15.1 --- a/src/HOL/Divides.thy	Thu Oct 12 18:09:06 2000 +0200
    15.2 +++ b/src/HOL/Divides.thy	Thu Oct 12 18:38:23 2000 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  The division operators div, mod and the divides relation "dvd"
    15.5  *)
    15.6  
    15.7 -Divides = Arith +
    15.8 +Divides = Arithmetic +
    15.9  
   15.10  (*We use the same class for div and mod;
   15.11    moreover, dvd is defined whenever multiplication is*)
    16.1 --- a/src/HOL/Fun.thy	Thu Oct 12 18:09:06 2000 +0200
    16.2 +++ b/src/HOL/Fun.thy	Thu Oct 12 18:38:23 2000 +0200
    16.3 @@ -6,7 +6,7 @@
    16.4  Notions about functions.
    16.5  *)
    16.6  
    16.7 -Fun = Vimage + equalities + 
    16.8 +Fun = Inverse_Image + equalities + 
    16.9  
   16.10  instance set :: (term) order
   16.11                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
    17.1 --- a/src/HOL/IOA/Asig.thy	Thu Oct 12 18:09:06 2000 +0200
    17.2 +++ b/src/HOL/IOA/Asig.thy	Thu Oct 12 18:38:23 2000 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  Action signatures
    17.5  *)
    17.6  
    17.7 -Asig = Prod +
    17.8 +Asig = Product_Type +
    17.9  
   17.10  types 
   17.11  
    18.1 --- a/src/HOL/Induct/Comb.ML	Thu Oct 12 18:09:06 2000 +0200
    18.2 +++ b/src/HOL/Induct/Comb.ML	Thu Oct 12 18:38:23 2000 +0200
    18.3 @@ -65,12 +65,12 @@
    18.4  
    18.5  Goal "x ---> y ==> x#z ---> y#z";
    18.6  by (etac rtrancl_induct 1);
    18.7 -by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
    18.8 +by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
    18.9  qed "Ap_reduce1";
   18.10  
   18.11  Goal "x ---> y ==> z#x ---> z#y";
   18.12  by (etac rtrancl_induct 1);
   18.13 -by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
   18.14 +by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
   18.15  qed "Ap_reduce2";
   18.16  
   18.17  (** Counterexample to the diamond property for -1-> **)
    19.1 --- a/src/HOL/Induct/LList.ML	Thu Oct 12 18:09:06 2000 +0200
    19.2 +++ b/src/HOL/Induct/LList.ML	Thu Oct 12 18:38:23 2000 +0200
    19.3 @@ -782,7 +782,7 @@
    19.4  by (ALLGOALS Asm_simp_tac);
    19.5  qed "fun_power_Suc";
    19.6  
    19.7 -val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
    19.8 +val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
    19.9   [("f","Pair")] (standard(refl RS cong RS cong));
   19.10  
   19.11  (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
    20.1 --- a/src/HOL/Induct/Sexp.thy	Thu Oct 12 18:09:06 2000 +0200
    20.2 +++ b/src/HOL/Induct/Sexp.thy	Thu Oct 12 18:38:23 2000 +0200
    20.3 @@ -7,7 +7,7 @@
    20.4  structures by hand.
    20.5  *)
    20.6  
    20.7 -Sexp = Univ + Inductive +
    20.8 +Sexp = Datatype_Universe + Inductive +
    20.9  consts
   20.10    sexp      :: 'a item set
   20.11  
    21.1 --- a/src/HOL/Inductive.thy	Thu Oct 12 18:09:06 2000 +0200
    21.2 +++ b/src/HOL/Inductive.thy	Thu Oct 12 18:38:23 2000 +0200
    21.3 @@ -2,7 +2,7 @@
    21.4      ID:         $Id$
    21.5  *)
    21.6  
    21.7 -theory Inductive = Gfp + Prod + Sum + NatDef
    21.8 +theory Inductive = Gfp + Sum_Type + NatDef
    21.9  files
   21.10    "Tools/induct_method.ML"
   21.11    "Tools/inductive_package.ML"
    22.1 --- a/src/HOL/Integ/IntDef.thy	Thu Oct 12 18:09:06 2000 +0200
    22.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Oct 12 18:38:23 2000 +0200
    22.3 @@ -6,7 +6,7 @@
    22.4  The integers as equivalence classes over nat*nat.
    22.5  *)
    22.6  
    22.7 -IntDef = Equiv + Arith +
    22.8 +IntDef = Equiv + Arithmetic +
    22.9  constdefs
   22.10    intrel      :: "((nat * nat) * (nat * nat)) set"
   22.11    "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
    23.1 --- a/src/HOL/IsaMakefile	Thu Oct 12 18:09:06 2000 +0200
    23.2 +++ b/src/HOL/IsaMakefile	Thu Oct 12 18:38:23 2000 +0200
    23.3 @@ -69,7 +69,7 @@
    23.4    $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
    23.5    $(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
    23.6    $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
    23.7 -  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \
    23.8 +  Arithmetic.ML Arithmetic.thy Calculation.thy Datatype.thy Divides.ML \
    23.9    Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
   23.10    HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
   23.11    Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
   23.12 @@ -80,17 +80,17 @@
   23.13    Integ/int_arith2.ML Integ/nat_simprocs.ML Lfp.ML Lfp.thy List.ML \
   23.14    List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
   23.15    NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
   23.16 -  Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy \
   23.17 -  RelPow.ML RelPow.thy Relation.ML Relation.thy Set.ML Set.thy \
   23.18 +  Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
   23.19 +  Relation_Power.ML Relation_Power.thy Relation.ML Relation.thy Set.ML Set.thy \
   23.20    SetInterval.ML SetInterval.thy String.thy SVC_Oracle.ML \
   23.21 -  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
   23.22 +  SVC_Oracle.thy Sum_Type.ML Sum_Type.thy Tools/datatype_aux.ML \
   23.23    Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   23.24    Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   23.25    Tools/induct_method.ML Tools/inductive_package.ML Tools/meson.ML \
   23.26    Tools/numeral_syntax.ML Tools/primrec_package.ML \
   23.27    Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
   23.28 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
   23.29 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy While.ML \
   23.30 +  Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy Datatype_Universe.ML Datatype_Universe.thy \
   23.31 +  Inverse_Image.ML Inverse_Image.thy Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML Wellfounded_Relations.thy While.ML \
   23.32    While.thy arith_data.ML blastdata.ML cladata.ML equalities.ML \
   23.33    equalities.thy hologic.ML meson_lemmas.ML mono.ML mono.thy simpdata.ML \
   23.34    subset.ML subset.thy thy_syntax.ML
    24.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Oct 12 18:09:06 2000 +0200
    24.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Oct 12 18:38:23 2000 +0200
    24.3 @@ -132,7 +132,7 @@
    24.4         rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
    24.5    apply (erule rtrancl_induct)
    24.6     apply blast
    24.7 -  apply (blast del: rtrancl_refl intro: rtranclIs)
    24.8 +  apply (blast del: rtrancl_refl intro: rtrancl_trans)
    24.9    done
   24.10  
   24.11  end
    25.1 --- a/src/HOL/Lfp.thy	Thu Oct 12 18:09:06 2000 +0200
    25.2 +++ b/src/HOL/Lfp.thy	Thu Oct 12 18:38:23 2000 +0200
    25.3 @@ -6,7 +6,7 @@
    25.4  The Knaster-Tarski Theorem
    25.5  *)
    25.6  
    25.7 -Lfp = mono + Prod +
    25.8 +Lfp = mono + Product_Type +
    25.9  
   25.10  constdefs
   25.11    lfp :: ['a set=>'a set] => 'a set
    26.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Thu Oct 12 18:09:06 2000 +0200
    26.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Thu Oct 12 18:38:23 2000 +0200
    26.3 @@ -13,19 +13,19 @@
    26.4  
    26.5  fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
    26.6  
    26.7 -val select_split = prove_goalw Prod.thy [split_def] 
    26.8 +val select_split = prove_goalw Product_Type.thy [split_def] 
    26.9  	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
   26.10  	 
   26.11  
   26.12 -val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
   26.13 +val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
   26.14  	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
   26.15 -val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
   26.16 +val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
   26.17  	(fn _ => [Auto_tac]);
   26.18 -val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
   26.19 +val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
   26.20  	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
   26.21  	rtac (split_beta RS subst) 1,
   26.22  	rtac (hd prems) 1]);
   26.23 -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 => [
   26.24 +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 => [
   26.25  	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
   26.26  	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
   26.27  	rtac (hd prems) 1]);
   26.28 @@ -131,11 +131,11 @@
   26.29  by(simp_tac (simpset() addsimps image_def::premises()) 1);
   26.30  qed "image_cong";
   26.31  
   26.32 -val split_Pair_eq = prove_goal Prod.thy 
   26.33 +val split_Pair_eq = prove_goal Product_Type.thy 
   26.34  "!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
   26.35  	etac imageE 1,
   26.36  	split_all_tac 1,
   26.37 -	auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
   26.38 +	auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
   26.39  
   26.40  
   26.41  (* More about Maps *)
    27.1 --- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Oct 12 18:09:06 2000 +0200
    27.2 +++ b/src/HOL/Modelcheck/MuckeSyn.ML	Thu Oct 12 18:38:23 2000 +0200
    27.3 @@ -147,7 +147,7 @@
    27.4  
    27.5  (* first simplification, then model checking *)
    27.6  
    27.7 -goalw Prod.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    27.8 +goalw Product_Type.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    27.9    by (rtac ext 1);
   27.10    by (stac (surjective_pairing RS sym) 1);
   27.11    by (rtac refl 1);
    28.1 --- a/src/HOL/NatDef.thy	Thu Oct 12 18:09:06 2000 +0200
    28.2 +++ b/src/HOL/NatDef.thy	Thu Oct 12 18:38:23 2000 +0200
    28.3 @@ -8,7 +8,7 @@
    28.4  Type nat is defined as a set Nat over type ind.
    28.5  *)
    28.6  
    28.7 -NatDef = WF +
    28.8 +NatDef = Wellfounded_Recursion +
    28.9  
   28.10  (** type ind **)
   28.11  
    29.1 --- a/src/HOL/PreList.thy	Thu Oct 12 18:09:06 2000 +0200
    29.2 +++ b/src/HOL/PreList.thy	Thu Oct 12 18:38:23 2000 +0200
    29.3 @@ -8,8 +8,8 @@
    29.4  *)
    29.5  
    29.6  theory PreList =
    29.7 -  Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
    29.8 -  SVC_Oracle + While:
    29.9 +  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
   29.10 +  Relation_Power + Calculation + SVC_Oracle + While:
   29.11  
   29.12  theorems [cases type: bool] = case_split
   29.13  
    30.1 --- a/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:09:06 2000 +0200
    30.2 +++ b/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:38:23 2000 +0200
    30.3 @@ -94,9 +94,9 @@
    30.4      [real_minus_add_distrib]));
    30.5  qed "sumr_minus";
    30.6  
    30.7 -context Arith.thy;
    30.8 +context Arithmetic.thy;
    30.9  
   30.10 -goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
   30.11 +Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
   30.12  by (auto_tac (claset() addSDs [not_leE],simpset()));
   30.13  qed "lemma_not_Suc_add";
   30.14  
    31.1 --- a/src/HOL/Recdef.thy	Thu Oct 12 18:09:06 2000 +0200
    31.2 +++ b/src/HOL/Recdef.thy	Thu Oct 12 18:38:23 2000 +0200
    31.3 @@ -5,7 +5,7 @@
    31.4  TFL: recursive function definitions.
    31.5  *)
    31.6  
    31.7 -theory Recdef = WF_Rel + Datatype
    31.8 +theory Recdef = Wellfounded_Relations + Datatype
    31.9  files
   31.10    "../TFL/utils.sml"
   31.11    "../TFL/usyntax.sml"
    32.1 --- a/src/HOL/Relation.thy	Thu Oct 12 18:09:06 2000 +0200
    32.2 +++ b/src/HOL/Relation.thy	Thu Oct 12 18:38:23 2000 +0200
    32.3 @@ -4,7 +4,7 @@
    32.4      Copyright   1996  University of Cambridge
    32.5  *)
    32.6  
    32.7 -Relation = Prod +
    32.8 +Relation = Product_Type +
    32.9  
   32.10  constdefs
   32.11    converse :: "('a*'b) set => ('b*'a) set"               ("(_^-1)" [1000] 999)
    33.1 --- a/src/HOL/SetInterval.thy	Thu Oct 12 18:09:06 2000 +0200
    33.2 +++ b/src/HOL/SetInterval.thy	Thu Oct 12 18:38:23 2000 +0200
    33.3 @@ -6,7 +6,7 @@
    33.4  lessThan, greaterThan, atLeast, atMost
    33.5  *)
    33.6  
    33.7 -SetInterval = equalities + Arith + 
    33.8 +SetInterval = equalities + Arithmetic + 
    33.9  
   33.10  constdefs
   33.11   lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    34.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:09:06 2000 +0200
    34.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:38:23 2000 +0200
    34.3 @@ -417,7 +417,7 @@
    34.4      val descr' = flat descr;
    34.5      val recTs = get_rec_types descr' sorts;
    34.6  
    34.7 -    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
    34.8 +    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
    34.9      val size_names = replicate (length (hd descr)) size_name @
   34.10        map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
   34.11          (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
    35.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 12 18:09:06 2000 +0200
    35.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 12 18:38:23 2000 +0200
    35.3 @@ -715,7 +715,7 @@
    35.4      val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    35.5        [descr] sorts thy7;
    35.6      val (thy9, size_thms) =
    35.7 -      if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
    35.8 +      if exists (equal "Arithmetic") (Sign.stamp_names_of (Theory.sign_of thy8)) then
    35.9          DatatypeAbsProofs.prove_size_thms false new_type_names
   35.10            [descr] sorts reccomb_names rec_thms thy8
   35.11        else (thy8, []);
    36.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:09:06 2000 +0200
    36.2 +++ b/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:38:23 2000 +0200
    36.3 @@ -398,7 +398,7 @@
    36.4      val descr' = flat descr;
    36.5      val recTs = get_rec_types descr' sorts;
    36.6  
    36.7 -    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
    36.8 +    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
    36.9      val size_names = replicate (length (hd descr)) size_name @
   36.10        map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
   36.11          (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
    37.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 12 18:09:06 2000 +0200
    37.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 12 18:38:23 2000 +0200
    37.3 @@ -185,7 +185,7 @@
    37.4  
    37.5  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
    37.6  
    37.7 -val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "vimage";
    37.8 +val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage";
    37.9  val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   37.10  
   37.11  (* make injections needed in mutually recursive definitions *)
    38.1 --- a/src/HOL/UNITY/Reach.ML	Thu Oct 12 18:09:06 2000 +0200
    38.2 +++ b/src/HOL/UNITY/Reach.ML	Thu Oct 12 18:38:23 2000 +0200
    38.3 @@ -31,7 +31,7 @@
    38.4  
    38.5  Goal "Rprg : Always reach_invariant";
    38.6  by (always_tac 1);
    38.7 -by (blast_tac (claset() addIs rtranclIs) 1);
    38.8 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    38.9  qed "reach_invariant";
   38.10  
   38.11  
   38.12 @@ -42,7 +42,7 @@
   38.13       "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
   38.14  by (rtac equalityI 1);
   38.15  by (auto_tac (claset() addSIs [ext], simpset()));
   38.16 -by (blast_tac (claset() addIs rtranclIs) 2);
   38.17 +by (blast_tac (claset() addIs [rtrancl_trans]) 2);
   38.18  by (etac rtrancl_induct 1);
   38.19  by Auto_tac;
   38.20  qed "fixedpoint_invariant_correct";
    39.1 --- a/src/HOL/ex/PiSets.thy	Thu Oct 12 18:09:06 2000 +0200
    39.2 +++ b/src/HOL/ex/PiSets.thy	Thu Oct 12 18:38:23 2000 +0200
    39.3 @@ -7,7 +7,7 @@
    39.4  Also the nice -> operator for function space
    39.5  *)
    39.6  
    39.7 -PiSets = Univ + Finite +
    39.8 +PiSets = Datatype_Universe + Finite +
    39.9  
   39.10  syntax
   39.11    "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    40.1 --- a/src/HOL/ex/cla.ML	Thu Oct 12 18:09:06 2000 +0200
    40.2 +++ b/src/HOL/ex/cla.ML	Thu Oct 12 18:38:23 2000 +0200
    40.3 @@ -462,7 +462,7 @@
    40.4  
    40.5  (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
    40.6    Fast_tac indeed copes!*)
    40.7 -goal Prod.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
    40.8 +goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
    40.9  \             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
   40.10  \             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
   40.11  by (Fast_tac 1);
   40.12 @@ -470,7 +470,7 @@
   40.13  
   40.14  (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   40.15    It does seem obvious!*)
   40.16 -goal Prod.thy
   40.17 +goal Product_Type.thy
   40.18      "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
   40.19  \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
   40.20  \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
   40.21 @@ -488,7 +488,7 @@
   40.22  by (Blast_tac 1);
   40.23  result();
   40.24  
   40.25 -goal Prod.thy
   40.26 +goal Product_Type.thy
   40.27      "(ALL x y. R(x,y) | R(y,x)) &                \
   40.28  \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
   40.29  \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
    41.1 --- a/src/HOL/ex/mesontest2.ML	Thu Oct 12 18:09:06 2000 +0200
    41.2 +++ b/src/HOL/ex/mesontest2.ML	Thu Oct 12 18:38:23 2000 +0200
    41.3 @@ -11,9 +11,9 @@
    41.4  (*All but the fastest are ignored to reduce build time*)
    41.5  val even_hard_ones = false;
    41.6  
    41.7 -(*Prod.thy instead of HOL.thy regards arguments as tuples.
    41.8 +(*Product_Type.thy instead of HOL.thy regards arguments as tuples.
    41.9    But Main.thy would allow clashes with many other constants*)
   41.10 -fun prove (s,tac) = prove_goal Prod.thy s (fn [] => [tac]);
   41.11 +fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
   41.12  
   41.13  fun prove_hard arg = if even_hard_ones then prove arg else TrueI;
   41.14  
    42.1 --- a/src/HOLCF/Cprod1.ML	Thu Oct 12 18:09:06 2000 +0200
    42.2 +++ b/src/HOLCF/Cprod1.ML	Thu Oct 12 18:38:23 2000 +0200
    42.3 @@ -3,7 +3,7 @@
    42.4      Author:     Franz Regensburger
    42.5      Copyright   1993  Technische Universitaet Muenchen
    42.6  
    42.7 -Partial ordering for cartesian product of HOL theory Prod.thy
    42.8 +Partial ordering for cartesian product of HOL theory Product_Type.thy
    42.9  *)
   42.10  
   42.11  
   42.12 @@ -15,7 +15,7 @@
   42.13  by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
   42.14  by (rotate_tac ~1 1);
   42.15  by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
   42.16 -by (asm_simp_tac (simpset_of Prod.thy) 1);
   42.17 +by (asm_simp_tac (simpset_of Product_Type.thy) 1);
   42.18  qed "Sel_injective_cprod";
   42.19  
   42.20  Goalw [less_cprod_def] "(p::'a*'b) << p";
    43.1 --- a/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Oct 12 18:09:06 2000 +0200
    43.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Oct 12 18:38:23 2000 +0200
    43.3 @@ -6,4 +6,4 @@
    43.4  Arithmetic lemmas
    43.5  *)
    43.6  
    43.7 -Lemmas = Arith
    43.8 +Lemmas = Arithmetic
    44.1 --- a/src/HOLCF/IOA/ABP/Packet.thy	Thu Oct 12 18:09:06 2000 +0200
    44.2 +++ b/src/HOLCF/IOA/ABP/Packet.thy	Thu Oct 12 18:38:23 2000 +0200
    44.3 @@ -6,7 +6,7 @@
    44.4  Packets
    44.5  *)
    44.6  
    44.7 -Packet = Arith +
    44.8 +Packet = Arithmetic +
    44.9  
   44.10  types
   44.11  
    45.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Oct 12 18:09:06 2000 +0200
    45.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Oct 12 18:38:23 2000 +0200
    45.3 @@ -35,7 +35,7 @@
    45.4  
    45.5  (* Arithmetic *)
    45.6  
    45.7 -goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
    45.8 +goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
    45.9  by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
   45.10  qed "pred_suc";
   45.11  
    46.1 --- a/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Oct 12 18:09:06 2000 +0200
    46.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Oct 12 18:38:23 2000 +0200
    46.3 @@ -6,4 +6,4 @@
    46.4  Arithmetic lemmas
    46.5  *)
    46.6  
    46.7 -Lemmas = Arith
    46.8 +Lemmas = Arithmetic
    47.1 --- a/src/HOLCF/IOA/NTP/Multiset.thy	Thu Oct 12 18:09:06 2000 +0200
    47.2 +++ b/src/HOLCF/IOA/NTP/Multiset.thy	Thu Oct 12 18:38:23 2000 +0200
    47.3 @@ -7,7 +7,7 @@
    47.4  Should be done as a subtype and moved to a global place.
    47.5  *)
    47.6  
    47.7 -Multiset = Arith + Lemmas +
    47.8 +Multiset = Lemmas +
    47.9  
   47.10  types
   47.11  
    48.1 --- a/src/HOLCF/IOA/NTP/Packet.thy	Thu Oct 12 18:09:06 2000 +0200
    48.2 +++ b/src/HOLCF/IOA/NTP/Packet.thy	Thu Oct 12 18:38:23 2000 +0200
    48.3 @@ -6,7 +6,7 @@
    48.4  Packets
    48.5  *)
    48.6  
    48.7 -Packet = Arith + Multiset +  
    48.8 +Packet = Multiset +  
    48.9  
   48.10  types
   48.11  
    49.1 --- a/src/HOLCF/Up1.thy	Thu Oct 12 18:09:06 2000 +0200
    49.2 +++ b/src/HOLCF/Up1.thy	Thu Oct 12 18:38:23 2000 +0200
    49.3 @@ -8,7 +8,7 @@
    49.4  
    49.5  *)
    49.6  
    49.7 -Up1 = Cfun3 + Sum + Datatype +
    49.8 +Up1 = Cfun3 + Sum_Type + Datatype +
    49.9  
   49.10  (* new type for lifting *)
   49.11