# HG changeset patch # User paulson # Date 886670819 -3600 # Node ID a0bdee64194c85b5654cfc996ba8731757f3b9e1 # Parent 0c32a609fcad4d061988c9d8c80b75d8d5f15354 Fixed a lot of overfull and underfull lines (hboxes) diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/classical.tex Thu Feb 05 10:26:59 1998 +0100 @@ -339,9 +339,12 @@ \index{simplification!from classical reasoner} The wrapper tacticals underly the operator addss, which combines each search step by simplification. Strictly speaking, \texttt{addss} is not part of the -classical reasoner. It should be defined (using \texttt{addSaltern - (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is -installed. +classical reasoner. It should be defined when the simplifier is +installed: +\begin{ttbox} +infix 4 addss; +fun cs addss ss = cs addbefore asm_full_simp_tac ss; +\end{ttbox} \begin{ttdescription} \item[$cs$ addss $ss$] \indexbold{*addss} @@ -396,7 +399,7 @@ instantiating quantifiers yourself. \begin{ttdescription} \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on -subgoal~$i$, using \texttt{clarify_step_tac}. +subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}. \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/defining.tex --- a/doc-src/Ref/defining.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/defining.tex Thu Feb 05 10:26:59 1998 +0100 @@ -85,7 +85,7 @@ \index{priority grammars|)} -\begin{figure} +\begin{figure}\small \begin{center} \begin{tabular}{rclc} $any$ &=& $prop$ ~~$|$~~ $logic$ \\\\ @@ -376,7 +376,7 @@ syntax trees. Section \S\ref{sec:asts} below discusses this obscure matter.\index{constants!for translations} - \item[{\tt parse_translation}, {\tt print_translation}] list sets + \item[{\tt parse_translation}, {\tt print_translation}] list the sets of constants that invoke translation functions for terms (see \S\ref{sec:tr_funs}). \end{description} diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/ref.ind Thu Feb 05 10:26:59 1998 +0100 @@ -217,12 +217,15 @@ \item {\tt Deriv.size}, \bold{49} \item {\tt Deriv.tree}, \bold{49} \item {\tt dest_eq}, \bold{101} + \item {\tt dest_imp}, \bold{101} \item {\tt dest_state}, \bold{41} + \item {\tt dest_Trueprop}, \bold{101} \item destruct-resolution, 18 \item {\tt DETERM}, \bold{33} \item discrimination nets, \bold{25} \item {\tt distinct_subgoals_tac}, \bold{23} \item {\tt dmatch_tac}, \bold{18} + \item {\tt domain_type}, \bold{102} \item {\tt dres_inst_tac}, \bold{19} \item {\tt dresolve_tac}, \bold{18} \item {\tt dtac}, \bold{20} @@ -240,7 +243,7 @@ \item {\tt eq_assume_tac}, \bold{18}, 131 \item {\tt eq_assumption}, \bold{47} \item {\tt eq_mp_tac}, \bold{138} - \item {\tt eq_reflection} theorem, \bold{101}, 122 + \item {\tt eq_reflection} theorem, \bold{102}, 122 \item {\tt eq_thm}, \bold{33} \item {\tt eq_thy}, \bold{58} \item {\tt equal_elim}, \bold{44} @@ -347,7 +350,7 @@ \item {\tt IF_UNSOLVED}, \bold{33} \item {\tt iff_reflection} theorem, 122 \item {\tt IFOL_ss}, \bold{125} - \item {\tt imp_intr} theorem, \bold{101} + \item {\tt imp_intr} theorem, \bold{102} \item {\tt implies_elim}, \bold{44} \item {\tt implies_elim_list}, \bold{44} \item {\tt implies_intr}, \bold{44} @@ -395,7 +398,7 @@ \item macros, 88--94 \item {\tt make_elim}, \bold{40}, 132 - \item {\tt Match} exception, 96, 101 + \item {\tt Match} exception, 95 \item {\tt match_tac}, \bold{18}, 131 \item {\tt max_pri}, 68, \bold{74} \item {\tt merge_ss}, \bold{106} @@ -451,9 +454,7 @@ \subitem renaming, 13, 22, 48 \item {\tt parents_of}, \bold{59} \item parse trees, 83 - \item {\tt parse_ast_translation}, 95 \item {\tt parse_rules}, 90 - \item {\tt parse_translation}, 95 \item pattern, higher-order, \bold{108} \item {\tt pause_tac}, \bold{27} \item Poly/{\ML} compiler, 5 @@ -470,7 +471,6 @@ \item {\tt prin}, 6, \bold{15} \item print mode, 52, 97 \item print modes, 78--79 - \item {\tt print_ast_translation}, 95 \item {\tt print_cs}, \bold{131} \item {\tt print_data}, \bold{59} \item {\tt print_depth}, \bold{4} @@ -485,7 +485,6 @@ \item {\tt print_tac}, \bold{27} \item {\tt print_theory}, \bold{59} \item {\tt print_thm}, \bold{38} - \item {\tt print_translation}, 95 \item printing control, 3--5 \item {\tt printyp}, \bold{15} \item priorities, 67, \bold{74} @@ -564,7 +563,7 @@ \item {\tt resolve_tac}, \bold{17}, 131 \item {\tt restore_proof}, \bold{15} \item {\tt result}, \bold{9}, 16, 57 - \item {\tt rev_mp} theorem, \bold{101} + \item {\tt rev_mp} theorem, \bold{102} \item rewrite rules, 107--108 \subitem permutative, 117--120 \item {\tt rewrite_goals_rule}, \bold{39} @@ -677,14 +676,14 @@ \item {\tt subgoal_tac}, \bold{20} \item {\tt subgoals_of_brl}, \bold{24} \item {\tt subgoals_tac}, \bold{20} - \item {\tt subst} theorem, 99, \bold{101} + \item {\tt subst} theorem, 99, \bold{102} \item substitution \subitem rules, 99 \item {\tt subthy}, \bold{58} \item {\tt swap} theorem, \bold{139} \item {\tt swap_res_tac}, \bold{138} \item {\tt swapify}, \bold{138} - \item {\tt sym} theorem, 100, \bold{101} + \item {\tt sym} theorem, 100, \bold{102} \item {\tt symmetric}, \bold{44} \item {\tt syn_of}, \bold{72} \item syntax @@ -772,6 +771,7 @@ \item {\tt theory} ML type, 51 \item {\tt Theory.add_oracle}, \bold{64} \item {\tt theory_of_thm}, \bold{41} + \item {\tt thin_refl} theorem, \bold{102} \item {\tt thin_tac}, \bold{23} \item {\tt THM} exception, 37, 38, 42, 47 \item {\tt thm} ML type, 37 @@ -827,7 +827,6 @@ \item type unknowns, \bold{63}, 70 \subitem freezing/thawing of, 46 \item type variables, \bold{63} - \item {\tt typed_print_translation}, 95 \item types, \bold{63} \subitem certified, \bold{63} \subitem printing of, 4, 15, 63 diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:59 1998 +0100 @@ -91,13 +91,13 @@ by (Asm_simp_tac 1); \end{ttbox} -\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet +\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet of tactics but may also loop where some of the others terminate. For example, \begin{ttbox} {\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} \end{ttbox} -is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt +is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} = g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not terminate. Isabelle notices certain simple forms of nontermination, @@ -366,10 +366,10 @@ \begin{ttdescription} -\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification +\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification procedures $procs$ to the current simpset. -\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification +\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification procedures $procs$ from the current simpset. \end{ttdescription} @@ -505,7 +505,7 @@ The solver is a pair of tactics that attempt to solve a subgoal after simplification. Typically it just proves trivial subgoals such as -{\tt True} and $t=t$. It could use sophisticated means such as {\tt +\texttt{True} and $t=t$. It could use sophisticated means such as {\tt blast_tac}, though that could make simplification expensive. Rewriting does not instantiate unknowns. For example, rewriting @@ -564,7 +564,7 @@ the solver. For this reason, solver tactics must be prepared to solve goals of the form $t = \Var{x}$, usually by reflexivity. In particular, reflexivity should be tried before any of the fancy -tactics like {\tt blast_tac}. +tactics like \texttt{blast_tac}. It may even happen that due to simplification the subgoal is no longer an equality. For example $False \bimp \Var{Q}$ could be rewritten to @@ -846,7 +846,7 @@ {\out val prem = "f(Suc(?n)) = Suc(f(?n))} {\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} \end{ttbox} -In the theorem~{\tt prem}, note that $f$ is a free variable while +In the theorem~\texttt{prem}, note that $f$ is a free variable while $\Var{n}$ is a schematic variable. \begin{ttbox} by (res_inst_tac [("n","i")] induct 1); @@ -958,7 +958,7 @@ \item To complete your set of rewrite rules, you must add not just associativity~(A) and commutativity~(C) but also a derived rule, {\bf - left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. + left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. \end{itemize} Ordered rewriting with the combination of A, C, and~LC sorts a term lexicographically: @@ -973,14 +973,14 @@ This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). Theory \thydx{Arith} contains natural numbers arithmetic. Its associated simpset contains many arithmetic laws including -distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list +distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let us prove the theorem \[ \sum@{i=1}^n i = n\times(n+1)/2. \] % -A functional~{\tt sum} represents the summation operator under the -interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We -extend {\tt Arith} as follows: +A functional~\texttt{sum} represents the summation operator under the +interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We +extend \texttt{Arith} as follows: \begin{ttbox} NatSum = Arith + consts sum :: [nat=>nat, nat] => nat @@ -997,7 +997,7 @@ Delsimprocs nat_cancel; Addsimps add_ac; \end{ttbox} -Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = +Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) = n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: \begin{ttbox} goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; @@ -1032,7 +1032,7 @@ {\out 2 * sum (\%i. i) (Suc n) = n * Suc n} {\out No subgoals!} \end{ttbox} -Simplification cannot prove the induction step if we omit {\tt add_ac} from +Simplification cannot prove the induction step if we omit \texttt{add_ac} from the simpset. Observe that like terms have not been collected: \begin{ttbox} {\out Level 3} @@ -1050,7 +1050,7 @@ \subsection{Re-orienting equalities} -Ordered rewriting with the derived rule {\tt symmetry} can reverse +Ordered rewriting with the derived rule \texttt{symmetry} can reverse equations: \begin{ttbox} val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" @@ -1058,16 +1058,16 @@ \end{ttbox} This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs in the conclusion but not~$s$, can often be brought into the right form. -For example, ordered rewriting with {\tt symmetry} can prove the goal +For example, ordered rewriting with \texttt{symmetry} can prove the goal \[ f(a)=b \conj f(a)=c \imp b=c. \] -Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ +Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$ because $f(a)$ is lexicographically greater than $b$ and~$c$. These re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the conclusion by~$f(a)$. Another example is the goal $\neg(t=u) \imp \neg(u=t)$. The differing orientations make this appear difficult to prove. Ordered -rewriting with {\tt symmetry} makes the equalities agree. (Without +rewriting with \texttt{symmetry} makes the equalities agree. (Without knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ or~$u=t$.) Then the simplifier can prove the goal outright. @@ -1126,7 +1126,8 @@ \begin{ttbox} local val lhss = - [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 0), []))]; + [read_cterm (sign_of Prod.thy) + ("f::'a*'b=>'c", TVar (("'z", 0), []))]; val rew = mk_meta_eq pair_eta_expand; \medskip fun proc _ _ (Abs _) = Some rew | proc _ _ _ = None; @@ -1165,10 +1166,10 @@ use "$ISABELLE_HOME/src/Provers/splitter.ML"; \end{ttbox} -Simplification requires reflecting various object-equalities to -meta-level rewrite rules. This demands rules stating that equal terms -and equivalent formulae are also equal at the meta-level. The rule -declaration part of the file {\tt FOL/IFOL.thy} contains the two lines +Simplification requires converting object-equalities to meta-level rewrite +rules. This demands rules stating that equal terms and equivalent formulae +are also equal at the meta-level. The rule declaration part of the file +\texttt{FOL/IFOL.thy} contains the two lines \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} eq_reflection "(x=y) ==> (x==y)" iff_reflection "(P<->Q) ==> (P==Q)" @@ -1177,7 +1178,7 @@ particular logic. In Constructive Type Theory, equality is a ternary relation of the form $a=b\in A$; the type~$A$ determines the meaning of the equality essentially as a partial equivalence relation. The -present simplifier cannot be used. Rewriting in {\tt CTT} uses +present simplifier cannot be used. Rewriting in \texttt{CTT} uses another simplifier, which resides in the file {\tt Provers/typedsimp.ML} and is not documented. Even this does not work for later variants of Constructive Type Theory that use @@ -1198,7 +1199,7 @@ (IntPr.fast_tac 1) ])); \end{ttbox} The following rewrite rules about conjunction are a selection of those -proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the +proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the standard simpset. \begin{ttbox} val conj_simps = map int_prove_fun @@ -1225,20 +1226,20 @@ setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4} \end{ttbox} The next step is to define the function for preprocessing rewrite rules. -This will be installed by calling {\tt setmksimps} below. Preprocessing +This will be installed by calling \texttt{setmksimps} below. Preprocessing occurs whenever rewrite rules are added, whether by user command or automatically. Preprocessing involves extracting atomic rewrites at the object-level, then reflecting them to the meta-level. -To start, the function {\tt gen_all} strips any meta-level +To start, the function \texttt{gen_all} strips any meta-level quantifiers from the front of the given theorem. Usually there are none anyway. \begin{ttbox} fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; \end{ttbox} -The function {\tt atomize} analyses a theorem in order to extract +The function \texttt{atomize} analyses a theorem in order to extract atomic rewrite rules. The head of all the patterns, matched by the -wildcard~{\tt _}, is the coercion function {\tt Trueprop}. +wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. \begin{ttbox} fun atomize th = case concl_of th of _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at @@ -1260,21 +1261,21 @@ \item Universal quantification: remove the quantifier, replacing the bound variable by a schematic variable, and extract rewrites from the body. -\item {\tt True} and {\tt False} contain no useful rewrites. +\item \texttt{True} and \texttt{False} contain no useful rewrites. \item Anything else: return the theorem in a singleton list. \end{itemize} The resulting theorems are not literally atomic --- they could be disjunctive, for example --- but are broken down as much as possible. See -the file {\tt ZF/simpdata.ML} for a sophisticated translation of +the file \texttt{ZF/simpdata.ML} for a sophisticated translation of set-theoretic formulae into rewrite rules. The simplified rewrites must now be converted into meta-equalities. The -rule {\tt eq_reflection} converts equality rewrites, while {\tt +rule \texttt{eq_reflection} converts equality rewrites, while {\tt iff_reflection} converts if-and-only-if rewrites. The latter possibility can arise in two other ways: the negative theorem~$\neg P$ is converted to -$P\equiv{\tt False}$, and any other theorem~$P$ is converted to -$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt +$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to +$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt iff_reflection_T} accomplish this conversion. \begin{ttbox} val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; @@ -1283,7 +1284,7 @@ val P_iff_T = int_prove_fun "P ==> (P <-> True)"; val iff_reflection_T = P_iff_T RS iff_reflection; \end{ttbox} -The function {\tt mk_meta_eq} converts a theorem to a meta-equality +The function \texttt{mk_meta_eq} converts a theorem to a meta-equality using the case analysis described above. \begin{ttbox} fun mk_meta_eq th = case concl_of th of @@ -1292,13 +1293,13 @@ | _ $ (Const("Not",_)$_) => th RS iff_reflection_F | _ => th RS iff_reflection_T; \end{ttbox} -The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will -be composed together and supplied below to {\tt setmksimps}. +The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will +be composed together and supplied below to \texttt{setmksimps}. \subsection{Making the initial simpset} -It is time to assemble these items. We open module {\tt Simplifier} +It is time to assemble these items. We open module \texttt{Simplifier} to gain direct access to its components. We define the infix operator \ttindex{addcongs} to insert congruence rules; given a list of theorems, it converts their conclusions into meta-equalities and @@ -1317,16 +1318,16 @@ fun ss addsplits splits = ss addloop (split_tac splits); \end{ttbox} -The list {\tt IFOL_simps} contains the default rewrite rules for -first-order logic. The first of these is the reflexive law expressed -as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is +The list \texttt{IFOL_simps} contains the default rewrite rules for +intuitionistic first-order logic. The first of these is the reflexive law +expressed as the equivalence $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless. \begin{ttbox} val IFOL_simps = [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at imp_simps \at iff_simps \at quant_simps; \end{ttbox} -The list {\tt triv_rls} contains trivial theorems for the solver. Any +The list \texttt{triv_rls} contains trivial theorems for the solver. Any subgoal that is simplified to one of these will be removed. \begin{ttbox} val notFalseI = int_prove_fun "~False"; @@ -1335,15 +1336,15 @@ % The basic simpset for intuitionistic \FOL{} is \ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt - gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified -subgoals using {\tt triv_rls} and assumptions, and by detecting + gen_all}, \texttt{atomize} and \texttt{mk_meta_eq}. It solves simplified +subgoals using \texttt{triv_rls} and assumptions, and by detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of conditional rewrites. -Other simpsets built from {\tt FOL_basic_ss} will inherit these items. +Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. In particular, \ttindexbold{IFOL_ss}, which introduces {\tt IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later -extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg +extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg P\bimp P$. \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} \index{*addsimps}\index{*addcongs} @@ -1355,20 +1356,22 @@ eq_assume_tac, ematch_tac [FalseE]]; val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac - addsimprocs [defALL_regroup,defEX_regroup] + addsimprocs [defALL_regroup, defEX_regroup] setSSolver safe_solver setSolver unsafe_solver - setmksimps (map mk_meta_eq o atomize o gen_all); + setmksimps (map mk_meta_eq o + atomize o gen_all); -val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps) +val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} + int_ex_simps {\at} int_all_simps) addcongs [imp_cong]; \end{ttbox} -This simpset takes {\tt imp_cong} as a congruence rule in order to use +This simpset takes \texttt{imp_cong} as a congruence rule in order to use contextual information to simplify the conclusions of implications: \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) \] -By adding the congruence rule {\tt conj_cong}, we could obtain a similar +By adding the congruence rule \texttt{conj_cong}, we could obtain a similar effect for conjunctions. @@ -1376,7 +1379,7 @@ To set up case splitting, we must prove the theorem \texttt{meta_iffD} below and pass it to \ttindexbold{mk_case_split_tac}. The tactic -\ttindexbold{split_tac} uses {\tt mk_meta_eq}, defined above, to +\ttindexbold{split_tac} uses \texttt{mk_meta_eq}, defined above, to convert the splitting rules to meta-equalities. \begin{ttbox} val meta_iffD = @@ -1399,7 +1402,7 @@ \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) \] Case splits should be allowed only when necessary; they are expensive -and hard to control. Here is an example of use, where {\tt expand_if} +and hard to control. Here is an example of use, where \texttt{expand_if} is the first rule above: \begin{ttbox} by (simp_tac (simpset() addloop (split_tac [expand_if])) 1); diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/syntax.tex --- a/doc-src/Ref/syntax.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/syntax.tex Thu Feb 05 10:26:59 1998 +0100 @@ -712,16 +712,13 @@ which triggers calls to it. Such names can be constants (logical or syntactic) or type constructors. -{\tt print_syntax} displays the sets of names associated with the -translation functions of a theory under -\ttindex{parse_ast_translation}, \ttindex{parse_translation}, -\ttindex{print_translation} (or \ttindex{typed_print_translation}) and -\ttindex{print_ast_translation}. You can add new ones via the {\tt - ML} section\index{*ML section} of a theory definition file. There -may never be more than one function of the same kind per name. Even -though the {\tt ML} section is the very last part of the file, newly -installed translation functions are already effective when processing -all of the preceding sections. +{\tt print_syntax} displays the sets of names associated with the translation +functions of a theory under \texttt{parse_ast_translation}, etc. You can add +new ones via the {\tt ML} section\index{*ML section} of a theory definition +file. There may never be more than one function of the same kind per name. +Even though the {\tt ML} section is the very last part of the file, newly +installed translation functions are already effective when processing all of +the preceding sections. The {\tt ML} section's contents are simply copied verbatim near the beginning of the \ML\ file generated from a theory definition file. diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/tactic.tex --- a/doc-src/Ref/tactic.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/tactic.tex Thu Feb 05 10:26:59 1998 +0100 @@ -475,7 +475,7 @@ proof state are never updated (see~\S\ref{match_tac}). \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] -returns the number of new subgoals that bi-resolution would yield for the +returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the pair (if applied to a suitable subgoal). This is $n$ if the flag is {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number of premises of the rule. Elim-resolution yields one fewer subgoal than diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/theories.tex Thu Feb 05 10:26:59 1998 +0100 @@ -838,7 +838,8 @@ \begin{ttbox} invoke_oracle : theory -> xstring -> Sign.sg * object -> thm -Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory +Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory + -> theory \end{ttbox} \begin{ttdescription} \item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)] @@ -914,8 +915,8 @@ Now in \texttt{IffOracle.ML} we first define a wrapper for invoking the oracle: \begin{ttbox} -fun iff_oracle n = - invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n); +fun iff_oracle n = invoke_oracle IffOracle.thy "iff" + (sign_of IffOracle.thy, IffOracleExn n); \end{ttbox} Here are some example applications of the \texttt{iff} oracle. An diff -r 0c32a609fcad -r a0bdee64194c doc-src/Ref/thm.tex --- a/doc-src/Ref/thm.tex Thu Feb 05 10:26:16 1998 +0100 +++ b/doc-src/Ref/thm.tex Thu Feb 05 10:26:59 1998 +0100 @@ -158,7 +158,7 @@ incorrectly. \item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}] - resembles \hbox{\tt read_instantiate {\it insts} {\it thm}}, but reads + is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads the instantiations under signature~{\it sg}. This is necessary to instantiate a rule from a general theory, such as first-order logic, using the notation of some specialized theory. Use the function {\tt @@ -226,7 +226,7 @@ tpairs_of : thm -> (term*term) list sign_of_thm : thm -> Sign.sg theory_of_thm : thm -> theory -dest_state : thm * int -> (term * term) list * term list * term * term +dest_state : thm * int -> (term*term) list * term list * term * term rep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, shyps: sort list, hyps: term list, prop: term\ttrbrace crep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, @@ -778,7 +778,7 @@ \begin{ttdescription} \item[\ttindexbold{keep_derivs} := MinDeriv $|$ ThmDeriv $|$ FullDeriv;] -specifies one of the three options for keeping derivations. They can be +specifies one of the options for keeping derivations. They can be minimal (oracles only), include theorems and axioms, or be full. \item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation,