diff -r fc6d5fa0ca3c -r e8cc166ba123 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Tue May 06 00:13:01 2008 +0200
+++ b/doc-src/IsarRef/logics.tex	Tue May 06 23:33:05 2008 +0200
@@ -1,89 +1,6 @@
 
 \chapter{Object-logic specific elements}\label{ch:logics}
 
-\section{General logic setup}\label{sec:object-logic}
-
-\indexisarcmd{judgment}
-\indexisarmeth{atomize}\indexisaratt{atomize}
-\indexisaratt{rule-format}\indexisaratt{rulify}
-
-\begin{matharray}{rcl}
-  \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
-  atomize & : & \isarmeth \\
-  atomize & : & \isaratt \\
-  rule_format & : & \isaratt \\
-  rulify & : & \isaratt \\
-\end{matharray}
-
-The very starting point for any Isabelle object-logic is a ``truth judgment''
-that links object-level statements to the meta-logic (with its minimal
-language of $prop$ that covers universal quantification $\Forall$ and
-implication $\Imp$).
-
-Common object-logics are sufficiently expressive to internalize rule
-statements over $\Forall$ and $\Imp$ within their own language.  This is
-useful in certain situations where a rule needs to be viewed as an atomic
-statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$
-versus $\forall x \in A. P(x)$.
-
-From the following language elements, only the $atomize$ method and
-$rule_format$ attribute are occasionally required by end-users, the rest is
-for those who need to setup their own object-logic.  In the latter case
-existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
-realistic examples.
-
-Generic tools may refer to the information provided by object-logic
-declarations internally.
-
-\railalias{ruleformat}{rule\_format}
-\railterm{ruleformat}
-
-\begin{rail}
-  'judgment' constdecl
-  ;
-  'atomize' ('(' 'full' ')')?
-  ;
-  ruleformat ('(' 'noasm' ')')?
-  ;
-\end{rail}
-
-\begin{descr}
-  
-\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the
-  truth judgment of the current object-logic.  Its type $\sigma$ should
-  specify a coercion of the category of object-level propositions to $prop$ of
-  the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link
-  the object language (internally of syntactic category $logic$) with that of
-  $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
-  theory development.
-  
-\item [$atomize$] (as a method) rewrites any non-atomic premises of a
-  sub-goal, using the meta-level equations declared via $atomize$ (as an
-  attribute) beforehand.  As a result, heavily nested goals become amenable to
-  fundamental operations such as resolution (cf.\ the $rule$ method) and
-  proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
-  here means to turn the whole subgoal into an object-statement (if possible),
-  including the outermost parameters and assumptions as well.
-
-  A typical collection of $atomize$ rules for a particular object-logic would
-  provide an internalization for each of the connectives of $\Forall$, $\Imp$,
-  and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
-  higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
-  should be covered as well (this is particularly important for locales, see
-  \S\ref{sec:locale}).
-
-\item [$rule_format$] rewrites a theorem by the equalities declared as
-  $rulify$ rules in the current object-logic.  By default, the result is fully
-  normalized, including assumptions and conclusions at any depth.  The
-  $no_asm$ option restricts the transformation to the conclusion of a rule.
-
-  In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
-  replace (bounded) universal quantification ($\forall$) and implication
-  ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
-
-\end{descr}
-
-
 \section{HOL}
 
 \subsection{Primitive types}\label{sec:hol-typedef}