removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;

--- a/doc-src/IsarRef/Makefile	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/IsarRef/Makefile	Tue Aug 28 12:31:53 2012 +0200
@@ -10,11 +10,10 @@
 NAME = isar-ref
 
 FILES = isar-ref.tex style.sty Thy/document/Framework.tex		\
-  Thy/document/Generic.tex Thy/document/HOLCF_Specific.tex		\
-  Thy/document/HOL_Specific.tex Thy/document/ML_Tactic.tex		\
-  Thy/document/Proof.tex Thy/document/Quick_Reference.tex		\
-  Thy/document/Spec.tex Thy/document/Synopsis.tex			\
-  Thy/document/Inner_Syntax.tex		\
+  Thy/document/Generic.tex Thy/document/HOL_Specific.tex		\
+  Thy/document/ML_Tactic.tex Thy/document/Proof.tex			\
+  Thy/document/Quick_Reference.tex Thy/document/Spec.tex		\
+  Thy/document/Synopsis.tex Thy/document/Inner_Syntax.tex		\
   Thy/document/Preface.tex Thy/document/Document_Preparation.tex	\
   Thy/document/Misc.tex Thy/document/Outer_Syntax.tex			\
   Thy/document/Symbols.tex ../isar.sty ../proof.sty ../iman.sty		\

--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Tue Aug 28 12:22:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-theory HOLCF_Specific
-imports Base HOLCF
-begin
-
-chapter {* Isabelle/HOLCF \label{ch:holcf} *}
-
-section {* Mixfix syntax for continuous operations *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
-  \end{matharray}
-
-  HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
-  \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
-  Isabelle mixfix syntax normally refers directly to the pure
-  meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
-  x"}.
-
-  The HOLCF variant of @{command (HOLCF) "consts"} modifies that of
-  Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
-  involving continuous function types are treated specifically.  Any
-  given syntax template is transformed internally, generating
-  translation rules for the abstract and concrete representation of
-  continuous application.  Note that mixing of HOLCF and Pure
-  application is \emph{not} supported!
-*}
-
-
-section {* Recursive domains *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
-  \end{matharray}
-
-  @{rail "
-    @@{command (HOLCF) domain} @{syntax parname}? (spec + @'and')
-    ;
-
-    spec: @{syntax typespec} '=' (cons + '|')
-    ;
-    cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
-    ;
-    dtrules: @'distinct' @{syntax thmrefs} @'inject' @{syntax thmrefs}
-      @'induction' @{syntax thmrefs}
-  "}
-
-  Recursive domains in HOLCF are analogous to datatypes in classical
-  HOL (cf.\ \secref{sec:hol-datatype}).  Mutual recursion is
-  supported, but no nesting nor arbitrary branching.  Domain
-  constructors may be strict (default) or lazy, the latter admits to
-  introduce infinitary objects in the typical LCF manner (e.g.\ lazy
-  lists).  See also \cite{MuellerNvOS99} for a general discussion of
-  HOLCF domains.
-*}
-
-end

--- a/doc-src/IsarRef/Thy/Preface.thy	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/IsarRef/Thy/Preface.thy	Tue Aug 28 12:31:53 2012 +0200
@@ -51,11 +51,10 @@
   \chref{ch:isar-framework}) works reasonably well for any Isabelle
   object-logic that conforms to the natural deduction view of the
   Isabelle/Pure framework.  Specific language elements introduced by
-  the major object-logics are described in \chref{ch:hol}
-  (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
-  (Isabelle/ZF).  The main language elements are already provided by
-  the Isabelle/Pure framework. Nevertheless, examples given in the
-  generic parts will usually refer to Isabelle/HOL as well.
+  Isabelle/HOL are described in \chref{ch:hol}.  Although the main
+  language elements are already provided by the Isabelle/Pure
+  framework, examples given in the generic parts will usually refer to
+  Isabelle/HOL.
 
   \medskip Isar commands may be either \emph{proper} document
   constructors, or \emph{improper commands}.  Some proof methods and

--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Tue Aug 28 12:22:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-quick_and_dirty := true;
-
-use_thy "HOLCF_Specific";

--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Tue Aug 28 12:22:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-quick_and_dirty := true;
-
-use_thy "ZF_Specific";

--- a/doc-src/IsarRef/Thy/document/Preface.tex	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Preface.tex	Tue Aug 28 12:31:53 2012 +0200
@@ -69,11 +69,10 @@
   \chref{ch:isar-framework}) works reasonably well for any Isabelle
   object-logic that conforms to the natural deduction view of the
   Isabelle/Pure framework.  Specific language elements introduced by
-  the major object-logics are described in \chref{ch:hol}
-  (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
-  (Isabelle/ZF).  The main language elements are already provided by
-  the Isabelle/Pure framework. Nevertheless, examples given in the
-  generic parts will usually refer to Isabelle/HOL as well.
+  Isabelle/HOL are described in \chref{ch:hol}.  Although the main
+  language elements are already provided by the Isabelle/Pure
+  framework, examples given in the generic parts will usually refer to
+  Isabelle/HOL.
 
   \medskip Isar commands may be either \emph{proper} document
   constructors, or \emph{improper commands}.  Some proof methods and

--- a/doc-src/IsarRef/isar-ref.tex	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Tue Aug 28 12:31:53 2012 +0200
@@ -69,9 +69,8 @@
 \input{Thy/document/Inner_Syntax.tex}
 \input{Thy/document/Misc.tex}
 \input{Thy/document/Generic.tex}
-\part{Object-Logics}
+\part{Object-Logic}
 \input{Thy/document/HOL_Specific.tex}
-\input{Thy/document/HOLCF_Specific.tex}
 
 \part{Appendix}
 \appendix

--- a/doc-src/ROOT	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/ROOT	Tue Aug 28 12:31:53 2012 +0200
@@ -82,7 +82,7 @@
     "document/build"
     "document/root.tex"
 
-session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
+session IsarRef (doc) in "IsarRef/Thy" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     quick_and_dirty, thy_output_source]
@@ -103,12 +103,6 @@
     Symbols
     ML_Tactic
 
-session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF +
-  options [browser_info = false, document = false,
-    document_dump = document, document_dump_mode = "tex",
-    quick_and_dirty, thy_output_source]
-  theories HOLCF_Specific
-
 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   options [document_variants = "sugar"]
   theories [document = ""]