--- a/NEWS Wed Apr 28 10:45:35 2004 +0200
+++ b/NEWS Thu Apr 29 06:01:20 2004 +0200
@@ -12,13 +12,21 @@
records), see also isar-ref manual. Potential INCOMPATIBILITY: need
to observe strictly sequential dependencies of definitions within a
single 'constdefs' section -- some existing specifications may have to
-be reordered.
+be reordered; moreover, the declared name needs to be an identifier.
+In the worst case may have to fall back on plain 'consts' + 'defs'.
* Pure: 'advanced' translation functions (parse_translation etc.) may
depend on the signature of the theory context being presently used for
parsing/printing, see also isar-ref manual.
+*** HOLCF ***
+
+* HOLCF: discontinued special version of 'constdefs' (which used to
+support continuous functions) in favor of the general Pure one with
+full type-inference.
+
+
New in Isabelle2004 (April 2004)
--------------------------------
--- a/doc-src/IsarRef/logics.tex Wed Apr 28 10:45:35 2004 +0200
+++ b/doc-src/IsarRef/logics.tex Thu Apr 29 06:01:20 2004 +0200
@@ -735,29 +735,22 @@
\subsection{Mixfix syntax for continuous operations}
-\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
+\indexisarcmdof{HOLCF}{consts}
\begin{matharray}{rcl}
\isarcmd{consts} & : & \isartrans{theory}{theory} \\
- \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
\end{matharray}
-\begin{rail}
- 'constdefs' (name '::' type mixfix? prop +)
- ;
-\end{rail}
-
HOLCF provides a separate type for continuous functions $\alpha \to
\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
syntax normally refers directly to the pure meta-level function type $\alpha
\To \beta$, with application $f\,x$.
-The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ resemble those of Pure
-Isabelle (cf.\ \S\ref{sec:consts}), although automated type-inference is not
-supported here. Internally, declarations involving continuous function types
-are treated specifically, transforming the syntax template accordingly and
-generating syntax translation rules for the abstract and concrete
-representation of application. Note that mixing continuous and meta-level
+The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\
+\S\ref{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!
\subsection{Recursive domains}
--- a/src/HOLCF/cont_consts.ML Wed Apr 28 10:45:35 2004 +0200
+++ b/src/HOLCF/cont_consts.ML Thu Apr 29 06:01:20 2004 +0200
@@ -3,16 +3,14 @@
Author: Tobias Mayr, David von Oheimb, and Markus Wenzel
License: GPL (GNU GENERAL PUBLIC LICENSE)
-HOLCF version of consts/constdefs: handle continuous function types in
-mixfix syntax.
+HOLCF version of consts: handle continuous function types in mixfix
+syntax.
*)
signature CONT_CONSTS =
sig
val add_consts: (bstring * string * mixfix) list -> theory -> theory
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
- val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
- val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
end;
structure ContConsts: CONT_CONSTS =
@@ -104,18 +102,6 @@
val add_consts_i = gen_add_consts Thm.ctyp_of;
-(* add_constdefs(_i) *)
-
-fun gen_add_constdefs consts defs args thy =
- thy
- |> consts (map fst args)
- |> defs (false, map (fn ((c, _, mx), s) =>
- ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
-
-fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args;
-fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args;
-
-
(* outer syntax *)
local structure P = OuterParse and K = OuterSyntax.Keyword in
@@ -124,12 +110,7 @@
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
(Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
-val constdefsP =
- OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl
- (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs));
-
-
-val _ = OuterSyntax.add_parsers [constsP, constdefsP];
+val _ = OuterSyntax.add_parsers [constsP];
end;