tuned;
authorwenzelm
Fri Sep 15 22:56:08 2006 +0200 (2006-09-15)
changeset 20547796ae7fa1049
parent 20546 8923deb735ad
child 20548 8ef25fe585a8
tuned;
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/document/tactic.tex
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
doc-src/IsarImplementation/Thy/proof.thy
doc-src/IsarImplementation/Thy/tactic.thy
doc-src/IsarImplementation/style.sty
src/HOL/Algebra/ringsimp.ML
src/HOL/Real/Float.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/res_atpset.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 15 20:08:38 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 15 22:56:08 2006 +0200
     1.3 @@ -134,6 +134,8 @@
     1.4    \indexmltype{typ}\verb|type typ| \\
     1.5    \indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
     1.6    \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
     1.7 +  \end{mldecls}
     1.8 +  \begin{mldecls}
     1.9    \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
    1.10    \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
    1.11    \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
    1.12 @@ -317,10 +319,12 @@
    1.13  \begin{mldecls}
    1.14    \indexmltype{term}\verb|type term| \\
    1.15    \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
    1.16 -  \indexml{map-term-types}\verb|map_term_types: (typ -> typ) -> term -> term| \\  %FIXME rename map_types
    1.17 +  \indexml{map-types}\verb|map_types: (typ -> typ) -> term -> term| \\
    1.18    \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
    1.19    \indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
    1.20    \indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
    1.21 +  \end{mldecls}
    1.22 +  \begin{mldecls}
    1.23    \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
    1.24    \indexml{lambda}\verb|lambda: term -> term -> term| \\
    1.25    \indexml{betapply}\verb|betapply: term * term -> term| \\
    1.26 @@ -341,7 +345,7 @@
    1.27    on type \verb|term|; raw datatype equality should only be used
    1.28    for operations related to parsing or printing!
    1.29  
    1.30 -  \item \verb|map_term_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
    1.31 +  \item \verb|map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
    1.32  
    1.33    \item \verb|fold_types|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term
    1.34    structure is traversed from left to right.
    1.35 @@ -574,10 +578,12 @@
    1.36  \begin{mldecls}
    1.37    \indexmltype{ctyp}\verb|type ctyp| \\
    1.38    \indexmltype{cterm}\verb|type cterm| \\
    1.39 +  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    1.40 +  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    1.41 +  \end{mldecls}
    1.42 +  \begin{mldecls}
    1.43    \indexmltype{thm}\verb|type thm| \\
    1.44    \indexml{proofs}\verb|proofs: int ref| \\
    1.45 -  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    1.46 -  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    1.47    \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
    1.48    \indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
    1.49    \indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
    1.50 @@ -587,6 +593,8 @@
    1.51    \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
    1.52    \indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
    1.53    \indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
    1.54 +  \end{mldecls}
    1.55 +  \begin{mldecls}
    1.56    \indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
    1.57    \indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
    1.58    \indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
    1.59 @@ -601,9 +609,13 @@
    1.60    well-typedness) checks, relative to the declarations of type
    1.61    constructors, constants etc. in the theory.
    1.62  
    1.63 -  This representation avoids syntactic rechecking in tight loops of
    1.64 -  inferences.  There are separate operations to decompose certified
    1.65 -  entities (including actual theorems).
    1.66 +  \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|cterm_of|~\isa{thy\ t} explicitly checks types and terms, respectively.  This also
    1.67 +  involves some basic normalizations, such expansion of type and term
    1.68 +  abbreviations from the theory context.
    1.69 +
    1.70 +  Re-certification is relatively slow and should be avoided in tight
    1.71 +  reasoning loops.  There are separate operations to decompose
    1.72 +  certified entities (including actual theorems).
    1.73  
    1.74    \item \verb|thm| represents proven propositions.  This is an
    1.75    abstract datatype that guarantees that its values have been
     2.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Sep 15 20:08:38 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Sep 15 22:56:08 2006 +0200
     2.3 @@ -177,7 +177,9 @@
     2.4    \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
     2.5    \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
     2.6    \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
     2.7 -  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
     2.8 +  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
     2.9 +  \end{mldecls}
    2.10 +  \begin{mldecls}
    2.11    \indexmltype{theory-ref}\verb|type theory_ref| \\
    2.12    \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
    2.13    \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
    2.14 @@ -555,7 +557,9 @@
    2.15    \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
    2.16    \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
    2.17    \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
    2.18 -  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
    2.19 +  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
    2.20 +  \end{mldecls}
    2.21 +  \begin{mldecls}
    2.22    \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
    2.23    \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
    2.24    \end{mldecls}
    2.25 @@ -634,7 +638,9 @@
    2.26  \begin{isamarkuptext}%
    2.27  \begin{mldecls}
    2.28    \indexml{Name.internal}\verb|Name.internal: string -> string| \\
    2.29 -  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
    2.30 +  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
    2.31 +  \end{mldecls}
    2.32 +  \begin{mldecls}
    2.33    \indexmltype{Name.context}\verb|type Name.context| \\
    2.34    \indexml{Name.context}\verb|Name.context: Name.context| \\
    2.35    \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
    2.36 @@ -805,11 +811,15 @@
    2.37    \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
    2.38    \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
    2.39    \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
    2.40 -  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
    2.41 +  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\
    2.42 +  \end{mldecls}
    2.43 +  \begin{mldecls}
    2.44    \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
    2.45    \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
    2.46    \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
    2.47 -  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
    2.48 +  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
    2.49 +  \end{mldecls}
    2.50 +  \begin{mldecls}
    2.51    \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
    2.52    \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
    2.53    \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
     3.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 15 20:08:38 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 15 22:56:08 2006 +0200
     3.3 @@ -329,10 +329,14 @@
     3.4    \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
     3.5  \verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
     3.6  \verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
     3.7 +  \end{mldecls}
     3.8 +  \begin{mldecls}
     3.9    \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
    3.10  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
    3.11    \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    3.12  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
    3.13 +  \end{mldecls}
    3.14 +  \begin{mldecls}
    3.15    \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
    3.16  \verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
    3.17    \end{mldecls}
     4.1 --- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Fri Sep 15 20:08:38 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Fri Sep 15 22:56:08 2006 +0200
     4.3 @@ -76,7 +76,7 @@
     4.4  
     4.5    \[
     4.6    \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
     4.7 -  \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
     4.8 +  \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{C}}{\isa{{\isacharhash}C}}
     4.9    \]
    4.10  
    4.11    \medskip The following low-level variants admit general reasoning
     5.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 20:08:38 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 22:56:08 2006 +0200
     5.3 @@ -123,6 +123,8 @@
     5.4    @{index_ML_type typ} \\
     5.5    @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
     5.6    @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
     5.7 +  \end{mldecls}
     5.8 +  \begin{mldecls}
     5.9    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
    5.10    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
    5.11    @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
    5.12 @@ -315,10 +317,12 @@
    5.13    \begin{mldecls}
    5.14    @{index_ML_type term} \\
    5.15    @{index_ML "op aconv": "term * term -> bool"} \\
    5.16 -  @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
    5.17 +  @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
    5.18    @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    5.19    @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
    5.20    @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    5.21 +  \end{mldecls}
    5.22 +  \begin{mldecls}
    5.23    @{index_ML fastype_of: "term -> typ"} \\
    5.24    @{index_ML lambda: "term -> term -> term"} \\
    5.25    @{index_ML betapply: "term * term -> term"} \\
    5.26 @@ -341,7 +345,7 @@
    5.27    on type @{ML_type term}; raw datatype equality should only be used
    5.28    for operations related to parsing or printing!
    5.29  
    5.30 -  \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
    5.31 +  \item @{ML map_types}~@{text "f t"} applies the mapping @{text
    5.32    "f"} to all types occurring in @{text "t"}.
    5.33  
    5.34    \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
    5.35 @@ -576,10 +580,12 @@
    5.36    \begin{mldecls}
    5.37    @{index_ML_type ctyp} \\
    5.38    @{index_ML_type cterm} \\
    5.39 +  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
    5.40 +  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
    5.41 +  \end{mldecls}
    5.42 +  \begin{mldecls}
    5.43    @{index_ML_type thm} \\
    5.44    @{index_ML proofs: "int ref"} \\
    5.45 -  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
    5.46 -  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
    5.47    @{index_ML Thm.assume: "cterm -> thm"} \\
    5.48    @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
    5.49    @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
    5.50 @@ -589,6 +595,8 @@
    5.51    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
    5.52    @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
    5.53    @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
    5.54 +  \end{mldecls}
    5.55 +  \begin{mldecls}
    5.56    @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
    5.57    @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
    5.58    @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
    5.59 @@ -603,9 +611,14 @@
    5.60    well-typedness) checks, relative to the declarations of type
    5.61    constructors, constants etc. in the theory.
    5.62  
    5.63 -  This representation avoids syntactic rechecking in tight loops of
    5.64 -  inferences.  There are separate operations to decompose certified
    5.65 -  entities (including actual theorems).
    5.66 +  \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
    5.67 +  t"} explicitly checks types and terms, respectively.  This also
    5.68 +  involves some basic normalizations, such expansion of type and term
    5.69 +  abbreviations from the theory context.
    5.70 +
    5.71 +  Re-certification is relatively slow and should be avoided in tight
    5.72 +  reasoning loops.  There are separate operations to decompose
    5.73 +  certified entities (including actual theorems).
    5.74  
    5.75    \item @{ML_type thm} represents proven propositions.  This is an
    5.76    abstract datatype that guarantees that its values have been
     6.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 20:08:38 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 22:56:08 2006 +0200
     6.3 @@ -152,7 +152,9 @@
     6.4    @{index_ML Theory.subthy: "theory * theory -> bool"} \\
     6.5    @{index_ML Theory.merge: "theory * theory -> theory"} \\
     6.6    @{index_ML Theory.checkpoint: "theory -> theory"} \\
     6.7 -  @{index_ML Theory.copy: "theory -> theory"} \\[1ex]
     6.8 +  @{index_ML Theory.copy: "theory -> theory"} \\
     6.9 +  \end{mldecls}
    6.10 +  \begin{mldecls}
    6.11    @{index_ML_type theory_ref} \\
    6.12    @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
    6.13    @{index_ML Theory.deref: "theory_ref -> theory"} \\
    6.14 @@ -480,7 +482,9 @@
    6.15    @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
    6.16    @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
    6.17    @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
    6.18 -  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
    6.19 +  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
    6.20 +  \end{mldecls}
    6.21 +  \begin{mldecls}
    6.22    @{index_ML_type "Symbol.sym"} \\
    6.23    @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
    6.24    \end{mldecls}
    6.25 @@ -552,7 +556,9 @@
    6.26  text %mlref {*
    6.27    \begin{mldecls}
    6.28    @{index_ML Name.internal: "string -> string"} \\
    6.29 -  @{index_ML Name.skolem: "string -> string"} \\[1ex]
    6.30 +  @{index_ML Name.skolem: "string -> string"} \\
    6.31 +  \end{mldecls}
    6.32 +  \begin{mldecls}
    6.33    @{index_ML_type Name.context} \\
    6.34    @{index_ML Name.context: Name.context} \\
    6.35    @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
    6.36 @@ -697,11 +703,15 @@
    6.37    @{index_ML NameSpace.qualifier: "string -> string"} \\
    6.38    @{index_ML NameSpace.append: "string -> string -> string"} \\
    6.39    @{index_ML NameSpace.pack: "string list -> string"} \\
    6.40 -  @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
    6.41 +  @{index_ML NameSpace.unpack: "string -> string list"} \\
    6.42 +  \end{mldecls}
    6.43 +  \begin{mldecls}
    6.44    @{index_ML_type NameSpace.naming} \\
    6.45    @{index_ML NameSpace.default_naming: NameSpace.naming} \\
    6.46    @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
    6.47 -  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
    6.48 +  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
    6.49 +  \end{mldecls}
    6.50 +  \begin{mldecls}
    6.51    @{index_ML_type NameSpace.T} \\
    6.52    @{index_ML NameSpace.empty: NameSpace.T} \\
    6.53    @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
     7.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Fri Sep 15 20:08:38 2006 +0200
     7.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Fri Sep 15 22:56:08 2006 +0200
     7.3 @@ -290,10 +290,14 @@
     7.4    "({context: Proof.context, schematics: ctyp list * cterm list,
     7.5      params: cterm list, asms: cterm list, concl: cterm,
     7.6      prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
     7.7 +  \end{mldecls}
     7.8 +  \begin{mldecls}
     7.9    @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
    7.10    ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
    7.11    @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
    7.12    ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
    7.13 +  \end{mldecls}
    7.14 +  \begin{mldecls}
    7.15    @{index_ML Obtain.result: "(Proof.context -> tactic) ->
    7.16    thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
    7.17    \end{mldecls}
     8.1 --- a/doc-src/IsarImplementation/Thy/tactic.thy	Fri Sep 15 20:08:38 2006 +0200
     8.2 +++ b/doc-src/IsarImplementation/Thy/tactic.thy	Fri Sep 15 22:56:08 2006 +0200
     8.3 @@ -61,7 +61,7 @@
     8.4  
     8.5    \[
     8.6    \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
     8.7 -  \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
     8.8 +  \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
     8.9    \]
    8.10  
    8.11    \medskip The following low-level variants admit general reasoning
     9.1 --- a/doc-src/IsarImplementation/style.sty	Fri Sep 15 20:08:38 2006 +0200
     9.2 +++ b/doc-src/IsarImplementation/style.sty	Fri Sep 15 22:56:08 2006 +0200
     9.3 @@ -37,7 +37,7 @@
     9.4  
     9.5  \renewcommand{\isadigit}[1]{\isamath{#1}}
     9.6  
     9.7 -\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
     9.8 +\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
     9.9  
    9.10  \isafoldtag{FIXME}
    9.11  \isakeeptag{mlref}
    10.1 --- a/src/HOL/Algebra/ringsimp.ML	Fri Sep 15 20:08:38 2006 +0200
    10.2 +++ b/src/HOL/Algebra/ringsimp.ML	Fri Sep 15 22:56:08 2006 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  signature ALGEBRA =
    10.5  sig
    10.6    val print_structures: Context.generic -> unit
    10.7 -  val setup: Theory.theory -> Theory.theory
    10.8 +  val setup: theory -> theory
    10.9  end;
   10.10  
   10.11  structure Algebra: ALGEBRA =
   10.12 @@ -17,7 +17,7 @@
   10.13  
   10.14  (** Theory and context data **)
   10.15  
   10.16 -fun struct_eq ((s1, ts1), (s2, ts2)) =
   10.17 +fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   10.18    (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
   10.19  
   10.20  structure AlgebraData = GenericDataFun
    11.1 --- a/src/HOL/Real/Float.ML	Fri Sep 15 20:08:38 2006 +0200
    11.2 +++ b/src/HOL/Real/Float.ML	Fri Sep 15 22:56:08 2006 +0200
    11.3 @@ -458,7 +458,7 @@
    11.4  			 end
    11.5  		       | _ => raise exn
    11.6  		    )
    11.7 -val th = ref ([]: Theory.theory list)
    11.8 +val th = ref ([]: theory list)
    11.9  val sg = ref ([]: Sign.sg list)
   11.10  
   11.11  fun invoke_float_op c = 
   11.12 @@ -507,4 +507,4 @@
   11.13  	invoke_oracle th "nat_op" (sg, Nat_op_oracle_data c)
   11.14      end
   11.15  *)
   11.16 -end;
   11.17 \ No newline at end of file
   11.18 +end;
    12.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 20:08:38 2006 +0200
    12.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 22:56:08 2006 +0200
    12.3 @@ -42,8 +42,8 @@
    12.4  
    12.5  	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    12.6  
    12.7 -	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
    12.8 -	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
    12.9 +	val make_cnf_thm  : theory -> Term.term -> Thm.thm
   12.10 +	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
   12.11  	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
   12.12  	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
   12.13  end;
   12.14 @@ -176,8 +176,6 @@
   12.15  (* inst_thm: instantiates a theorem with a list of terms                     *)
   12.16  (* ------------------------------------------------------------------------- *)
   12.17  
   12.18 -(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
   12.19 -
   12.20  fun inst_thm thy ts thm =
   12.21  	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
   12.22  
    13.1 --- a/src/HOL/Tools/res_atpset.ML	Fri Sep 15 20:08:38 2006 +0200
    13.2 +++ b/src/HOL/Tools/res_atpset.ML	Fri Sep 15 22:56:08 2006 +0200
    13.3 @@ -84,7 +84,7 @@
    13.4    val extend = copy;
    13.5    fun merge _ (ref atpst1, ref atpst2) =
    13.6        ref (merge_atpset (atpst1, atpst2));
    13.7 -  fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
    13.8 +  fun print _ (ref atpst) = print_atpset atpst;
    13.9  end);
   13.10  
   13.11  val print_AtpSet = GlobalAtpSet.print; 
   13.12 @@ -138,4 +138,4 @@
   13.13  
   13.14  val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
   13.15  
   13.16 -end;
   13.17 \ No newline at end of file
   13.18 +end;