# HG changeset patch # User wenzelm # Date 1346149913 -7200 # Node ID c04001b3a753bb1a950abac6d20ccb7310c7b4ab # Parent d54a3d39ba85f4cd95e9944dadf8d0ab814b804a removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only; diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Makefile --- 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 \ diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/HOLCF_Specific.thy --- 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 \ theory"} \\ - \end{matharray} - - HOLCF provides a separate type for continuous functions @{text "\ \ - \"}, with an explicit application operator @{term "f \ x"}. - Isabelle mixfix syntax normally refers directly to the pure - meta-level function type @{text "\ \ \"}, 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 \ 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 diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/Preface.thy --- 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 diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/ROOT-HOLCF.ML --- 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"; diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/ROOT-ZF.ML --- 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"; diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/document/Preface.tex --- 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 diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/isar-ref.tex --- 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 diff -r d54a3d39ba85 -r c04001b3a753 doc-src/ROOT --- 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 = ""]