merged
authornipkow
Wed, 19 Oct 2011 16:32:30 +0200
changeset 45201 154242732ef8
parent 45196 78478d938cb8 (diff)
parent 45200 1f1897ac7877 (current diff)
child 45202 62b8bcf24773
merged
--- a/Admin/isatest/isatest-stats	Wed Oct 19 16:32:12 2011 +0200
+++ b/Admin/isatest/isatest-stats	Wed Oct 19 16:32:30 2011 +0200
@@ -8,161 +8,177 @@
 
 PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
 
-ISABELLE_SESSIONS="\
-  HOL-Auth \
-  HOL-Bali \
-  HOL-Boogie-Examples \
-  HOL-Decision_Procs \
-  HOL-Hahn_Banach \
-  HOL-Hoare \
-  HOL-Hoare_Parallel \
-  HOL-IMPP \
-  HOL-IOA \
-  HOL-Imperative_HOL \
-  HOL-Import \
-  HOL-Induct \
-  HOL-Isar_Examples \
-  HOL-Lattice \
-  HOL-Library-Codegenerator_Test \
-  HOL-Matrix \
-  HOL-Metis_Examples \
-  HOL-MicroJava \
-  HOL-Mirabelle \
-  HOL-Mutabelle \
-  HOL-NanoJava \
-  HOL-Nitpick_Examples \
+ISABELLE_SESSIONS="
+  HOL
+  HOL-Main
+  HOL-Plain
+  HOL-Base
+  HOL-Library
+  HOL-Algebra
+  HOL-Auth
+  HOL-Bali
+  HOL-Boogie
+  HOL-Boogie-Examples
+  HOL-Decision_Procs
+  HOL-Hahn_Banach
+  HOL-Hoare
+  HOL-Hoare_Parallel
+  HOL-IMP
+  HOL-IMPP
+  HOL-IOA
+  HOL-Imperative_HOL
+  HOL-Import
+  HOL-Induct
+  HOL-Isar_Examples
+  HOL-Lattice
+  HOL-Library-Codegenerator_Test
+  HOL-Matrix
+  HOL-Metis_Examples
+  HOL-MicroJava
+  HOL-Mirabelle
+  HOL-Multivariate_Analysis
+  HOL-Mutabelle
+  HOL-NSA
+  HOL-NanoJava
+  HOL-Nitpick_Examples
+  HOL-Nominal
   HOL-Nominal-Examples
-  HOL-Number_Theory \
-  HOL-Old_Number_Theory \
-  HOL-Predicate_Compile_Examples \
+  HOL-Number_Theory
+  HOL-Old_Number_Theory
+  HOL-Predicate_Compile_Examples
   HOL-Probability
-  HOL-Prolog \
-  HOL-Proofs-Extraction \
-  HOL-Proofs-Lambda \
-  HOL-Proofs-ex \
-  HOL-Quotient_Examples \
-  HOL-SET_Protocol \
-  HOL-SPARK-Examples \
-  HOL-SPARK-Manual \
-  HOL-Statespace \
-  HOL-TPTP \
-  HOL-UNITY \
-  HOL-Unix \
-  HOL-Word-Examples \
-  HOL-Word-SMT_Examples \
+  HOL-Prolog
+  HOL-Proofs
+  HOL-Proofs-Extraction
+  HOL-Proofs-Lambda
+  HOL-Proofs-ex
+  HOL-Quotient_Examples
+  HOL-SET_Protocol
+  HOL-SPARK
+  HOL-SPARK-Examples
+  HOL-SPARK-Manual
+  HOL-Statespace
+  HOL-TPTP
+  HOL-UNITY
+  HOL-Unix
+  HOL-Word
+  HOL-Word-Examples
+  HOL-Word-SMT_Examples
   HOL-ZF
-  HOL-ex \
-  HOLCF-FOCUS \
-  HOLCF-IMP \
-  HOLCF-Library \
-  HOLCF-Tutorial \
-  HOLCF-ex \
-  IOA-ABP \
-  IOA-NTP \
-  IOA-Storage \
-  IOA-ex \
-  TLA-Buffer \
-  TLA-Inc \
+  HOL-ex
+  HOL4
+  HOLCF
+  HOLCF-FOCUS
+  HOLCF-IMP
+  HOLCF-Library
+  HOLCF-Tutorial
+  HOLCF-ex
+  IOA
+  IOA-ABP
+  IOA-NTP
+  IOA-Storage
+  IOA-ex
+  TLA
+  TLA-Buffer
+  TLA-Inc
   TLA-Memory"
 
-AFP_SESSIONS="\
-  ArrowImpossibilityGS \
-  Coinductive \
-  CoreC++ \
-  HOL-AVL-Trees \
-  HOL-Abstract-Hoare-Logics \
-  HOL-Abstract-Rewriting \
-  HOL-BinarySearchTree \
-  HOL-Binomial-Heaps \
-  HOL-Binomial-Queues \
-  HOL-BytecodeLogicJmlTypes \
-  HOL-Category \
-  HOL-Category2 \
-  HOL-Cauchy \
-  HOL-ClockSynchInst \
-  HOL-CofGroups \
-  HOL-Collections \
-  HOL-Compiling-Exceptions-Correctly \
-  HOL-Completeness \
-  HOL-DPT-SAT-Solver \
-  HOL-DataRefinementIBP \
-  HOL-Depth-First-Search \
-  HOL-DiskPaxos \
-  HOL-Example-Submission \
-  HOL-FFT \
-  HOL-FOL-Fitting \
-  HOL-FeatherweightJava \
-  HOL-FileRefinement \
-  HOL-FinFun \
-  HOL-Finger-Trees \
-  HOL-Flyspeck-Tame \
-  HOL-Free-Boolean-Algebra \
-  HOL-Free-Groups \
-  HOL-FunWithFunctions \
-  HOL-FunWithTilings \
-  HOL-Functional-Automata \
-  HOL-Gauss-Jordan-Elim-Fun \
-  HOL-GenClock \
-  HOL-General-Triangle \
-  HOL-GraphMarkingIBP \
-  HOL-HotelKeyCards \
-  HOL-Huffman \
-  HOL-Integration \
-  HOL-JiveDataStoreModel \
-  HOL-KBPs \
-  HOL-Lazy-Lists-II \
-  HOL-LightweightJava \
-  HOL-List-Index \
-  HOL-Locally-Nameless-Sigma \
-  HOL-Marriage \
-  HOL-Matrix \
-  HOL-Max-Card-Matching \
-  HOL-MiniML \
-  HOL-MuchAdoAboutTwo \
-  HOL-Multivariate_Analysis \
-  HOL-Myhill-Nerode \
-  HOL-Nominal \
-  HOL-Nominal-Lam-ml-Normalization \
-  HOL-Nominal-SequentInvertibility \
-  HOL-Ordinal \
-  HOL-Ordinals_and_Cardinals \
-  HOL-POPLmark-deBruijn \
-  HOL-Perfect-Number-Thm \
-  HOL-Polynomials \
-  HOL-Presburger-Automata \
-  HOL-Program-Conflict-Analysis \
-  HOL-Ramsey-Infinite \
-  HOL-Recursion-Theory-I \
-  HOL-Regular-Sets \
-  HOL-Robbins-Conjecture \
-  HOL-SATSolverVerification \
-  HOL-SIFPL \
-  HOL-SenSocialChoice \
-  HOL-Statecharts \
-  HOL-Topology \
-  HOL-Transitive-Closure \
-  HOL-Tree-Automata \
-  HOL-Verified-Prover \
-  HOL-Word \
-  HOL-Word-RIPEMD-160-SPARK \
-  HOLCF \
-  HOLCF-Shivers-CFA \
-  HOLCF-Stream-Fusion \
-  HOLCF-WorkerWrapper \
-  HRB-Slicing \
-  HRB-Slicing-InformationFlowSlicing \
-  Jinja \
-  Jinja \
-  LatticeProperties \
-  LatticeProperties-MonoBoolTranAlgebra \
-  LatticeProperties-PseudoHoops \
-  Lower_Semicontinuous \
-  NormByEval \
-  Simpl \
-  Simpl-BDD \
-  Slicing \
-  Slicing \
-  Slicing-InformationFlowSlicing \
+AFP_SESSIONS="
+  ArrowImpossibilityGS
+  Coinductive
+  CoreC++
+  HOL-AVL-Trees
+  HOL-Abstract-Hoare-Logics
+  HOL-Abstract-Rewriting
+  HOL-BinarySearchTree
+  HOL-Binomial-Heaps
+  HOL-Binomial-Queues
+  HOL-BytecodeLogicJmlTypes
+  HOL-Category
+  HOL-Category2
+  HOL-Cauchy
+  HOL-ClockSynchInst
+  HOL-CofGroups
+  HOL-Collections
+  HOL-Compiling-Exceptions-Correctly
+  HOL-Completeness
+  HOL-DPT-SAT-Solver
+  HOL-DataRefinementIBP
+  HOL-Depth-First-Search
+  HOL-DiskPaxos
+  HOL-Example-Submission
+  HOL-FFT
+  HOL-FOL-Fitting
+  HOL-FeatherweightJava
+  HOL-FileRefinement
+  HOL-FinFun
+  HOL-Finger-Trees
+  HOL-Flyspeck-Tame
+  HOL-Free-Boolean-Algebra
+  HOL-Free-Groups
+  HOL-FunWithFunctions
+  HOL-FunWithTilings
+  HOL-Functional-Automata
+  HOL-Gauss-Jordan-Elim-Fun
+  HOL-GenClock
+  HOL-General-Triangle
+  HOL-GraphMarkingIBP
+  HOL-HotelKeyCards
+  HOL-Huffman
+  HOL-Integration
+  HOL-JiveDataStoreModel
+  HOL-KBPs
+  HOL-Lazy-Lists-II
+  HOL-LightweightJava
+  HOL-List-Index
+  HOL-Locally-Nameless-Sigma
+  HOL-Marriage
+  HOL-Matrix
+  HOL-Max-Card-Matching
+  HOL-MiniML
+  HOL-MuchAdoAboutTwo
+  HOL-Multivariate_Analysis
+  HOL-Myhill-Nerode
+  HOL-Nominal
+  HOL-Nominal-Lam-ml-Normalization
+  HOL-Nominal-SequentInvertibility
+  HOL-Ordinal
+  HOL-Ordinals_and_Cardinals
+  HOL-POPLmark-deBruijn
+  HOL-Perfect-Number-Thm
+  HOL-Polynomials
+  HOL-Presburger-Automata
+  HOL-Program-Conflict-Analysis
+  HOL-Ramsey-Infinite
+  HOL-Recursion-Theory-I
+  HOL-Regular-Sets
+  HOL-Robbins-Conjecture
+  HOL-SATSolverVerification
+  HOL-SIFPL
+  HOL-SenSocialChoice
+  HOL-Statecharts
+  HOL-Topology
+  HOL-Transitive-Closure
+  HOL-Tree-Automata
+  HOL-Verified-Prover
+  HOL-Word
+  HOL-Word-RIPEMD-160-SPARK
+  HOLCF
+  HOLCF-Shivers-CFA
+  HOLCF-Stream-Fusion
+  HOLCF-WorkerWrapper
+  HRB-Slicing
+  HRB-Slicing-InformationFlowSlicing
+  Jinja
+  LatticeProperties
+  LatticeProperties-MonoBoolTranAlgebra
+  LatticeProperties-PseudoHoops
+  Lower_Semicontinuous
+  NormByEval
+  Simpl
+  Simpl-BDD
+  Slicing
+  Slicing-InformationFlowSlicing
   VolpanoSmith"
 
 
--- a/NEWS	Wed Oct 19 16:32:12 2011 +0200
+++ b/NEWS	Wed Oct 19 16:32:30 2011 +0200
@@ -28,6 +28,7 @@
   zadd_commute ~> add_commute
   zadd_assoc ~> add_assoc
   zadd_left_commute ~> add_left_commute
+  zadd_ac ~> add_ac
   zmult_ac ~> mult_ac
   zadd_0 ~> add_0_left
   zadd_0_right ~> add_0_right
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Oct 19 16:32:12 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Oct 19 16:32:30 2011 +0200
@@ -1724,17 +1724,12 @@
   A more efficient way of executing specifications is to translate
   them into a functional programming language such as ML.
 
-  Isabelle provides two generic frameworks to support code generation
+  Isabelle provides a generic framework to support code generation
   from executable specifications.  Isabelle/HOL instantiates these
-  mechanisms in a way that is amenable to end-user applications.
-*}
-
-
-subsection {* The new code generator (F. Haftmann) *}
-
-text {* This framework generates code from functional programs
-  (including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+  mechanisms in a way that is amenable to end-user applications.  Code
+  can be generated for functional programs (including overloading
+  using type classes) targeting SML \cite{SML}, OCaml \cite{OCaml},
+  Haskell \cite{haskell-revised-report} and Scala
   \cite{scala-overview-tech-report}.  Conceptually, code generation is
   split up in three steps: \emph{selection} of code theorems,
   \emph{translation} into an abstract executable view and
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Oct 19 16:32:12 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Oct 19 16:32:30 2011 +0200
@@ -2523,20 +2523,12 @@
   A more efficient way of executing specifications is to translate
   them into a functional programming language such as ML.
 
-  Isabelle provides two generic frameworks to support code generation
+  Isabelle provides a generic framework to support code generation
   from executable specifications.  Isabelle/HOL instantiates these
-  mechanisms in a way that is amenable to end-user applications.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{The new code generator (F. Haftmann)%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This framework generates code from functional programs
-  (including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+  mechanisms in a way that is amenable to end-user applications.  Code
+  can be generated for functional programs (including overloading
+  using type classes) targeting SML \cite{SML}, OCaml \cite{OCaml},
+  Haskell \cite{haskell-revised-report} and Scala
   \cite{scala-overview-tech-report}.  Conceptually, code generation is
   split up in three steps: \emph{selection} of code theorems,
   \emph{translation} into an abstract executable view and
@@ -2989,388 +2981,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{The old code generator (S. Berghofer)%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This framework generates code from both functional and
-  relational programs to SML, as explained below.
-
-  \begin{matharray}{rcl}
-    \indexdef{}{command}{code\_module}\hypertarget{command.code-module}{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{}{command}{code\_library}\hypertarget{command.code-library}{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{}{command}{consts\_code}\hypertarget{command.consts-code}{\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{}{command}{types\_code}\hypertarget{command.types-code}{\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
-  \end{matharray}
-
-  \begin{railoutput}
-\rail@begin{11}{}
-\rail@bar
-\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{modespec}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
-\rail@nextbar{4}
-\rail@term{\isa{\isakeyword{file}}}[]
-\rail@nont{\isa{name}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{4}
-\rail@term{\isa{\isakeyword{imports}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextplus{5}
-\rail@endplus
-\rail@endbar
-\rail@cr{7}
-\rail@term{\isa{\isakeyword{contains}}}[]
-\rail@bar
-\rail@plus
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{8}
-\rail@endplus
-\rail@nextbar{9}
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{10}
-\rail@endplus
-\rail@endbar
-\rail@end
-\rail@begin{2}{\isa{modespec}}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@endplus
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
-\rail@plus
-\rail@nont{\isa{codespec}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{codespec}}
-\rail@nont{\isa{const}}[]
-\rail@nont{\isa{template}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{attachment}}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
-\rail@plus
-\rail@nont{\isa{tycodespec}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{tycodespec}}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nont{\isa{template}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{attachment}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{\isa{const}}
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{1}{\isa{template}}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{2}{\isa{attachment}}
-\rail@term{\isa{attach}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{modespec}}[]
-\rail@endbar
-\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
-\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
-\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{name}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Invoking the code generator%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}
-  and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to
-  \emph{incremental} and \emph{modular} code generation, respectively.
-
-  \begin{description}
-
-  \item [Modular] For each theory, an ML structure is generated,
-  containing the code generated from the constants defined in this
-  theory.
-
-  \item [Incremental] All the generated code is emitted into the same
-  structure.  This structure may import code from previously generated
-  structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.
-  Moreover, the generated structure may also be referred to in later
-  invocations of the code generator.
-
-  \end{description}
-
-  After the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}} and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}
-  keywords, the user may specify an optional list of ``modes'' in
-  parentheses. These can be used to instruct the code generator to
-  emit additional code for special purposes, e.g.\ functions for
-  converting elements of generated datatypes to Isabelle terms, or
-  test data generators. The list of modes is followed by a module
-  name.  The module name is optional for modular code generation, but
-  must be specified for incremental code generation.
-
-  The code can either be written to a file, in which case a file name
-  has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded
-  directly into Isabelle's ML environment. In the latter case, the
-  \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results
-  interactively, for example.
-
-  The terms from which to generate code can be specified after the
-  \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just
-  as a list of terms. In the latter case, the code generator just
-  produces code for all constants and types occuring in the term, but
-  does not bind the compiled terms to ML identifiers.
-
-  Here is an example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
-\ Test\isanewline
-\isakeyword{contains}\ test\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}foldl\ op\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent This binds the result of compiling the given term to
-  the ML identifier \verb|Test.test|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
-\isaantiq
-assert{}%
-\endisaantiq
-\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isamarkupsubsubsection{Configuring the code generator%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-When generating code for a complex term, the code generator
-  recursively calls itself for all subterms.  When it arrives at a
-  constant, the default strategy of the code generator is to look up
-  its definition and try to generate code for it.  Constants which
-  have no definitions that are immediately executable, may be
-  associated with a piece of ML code manually using the \indexref{}{command}{consts\_code}\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}} command.  It takes a list whose elements consist of a
-  constant (given in usual term syntax -- an explicit type constraint
-  accounts for overloading), and a mixfix template describing the ML
-  code. The latter is very much the same as the mixfix templates used
-  when declaring new constants.  The most notable difference is that
-  terms may be included in the ML template using antiquotation
-  brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.
-
-  A similar mechanism is available for types: \indexref{}{command}{types\_code}\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}} associates type constructors with specific ML code.
-
-  For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of
-  Isabelle/HOL should be compiled to ML.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline
-\isacommand{consts}\isamarkupfalse%
-\ Pair\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
-\ prod\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
-\ Pair\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptext}%
-Sometimes, the code associated with a constant or type may
-  need to refer to auxiliary functions, which have to be emitted when
-  the constant is used. Code for such auxiliary functions can be
-  declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}
-  function can be implemented as follows:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
-\ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline
-\isakeyword{attach}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ fun\ wfrec\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}wfrec\ f{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
-\begin{isamarkuptext}%
-If the code containing a call to \isa{wfrec} resides in an
-  ML structure different from the one containing the function
-  definition attached to \isa{wfrec}, the name of the ML structure
-  (followed by a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}'')  is inserted in place of ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}{\isaliteral{22}{\isachardoublequote}}}'' in the above template.  The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''  means that
-  the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not
-  executable.
-
-  \medskip Another possibility of configuring the code generator is to
-  register theorems to be used for code generation. Theorems can be
-  registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional
-  name as an argument, which indicates the format of the
-  theorem. Currently supported formats are equations (this is the
-  default when no name is specified) and horn clauses (this is
-  indicated by the name \texttt{ind}). The left-hand sides of
-  equations may only contain constructors and distinct variables,
-  whereas horn clauses must have the same format as introduction rules
-  of inductive definitions.
-
-  The following example specifies three equations from which to
-  generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also
-  \verb|~~/src/HOL/Nat.thy|).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Suc\ m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp{\isaliteral{5F}{\isacharunderscore}}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isamarkupsubsubsection{Specific HOL code generators%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The basic code generator framework offered by Isabelle/Pure
-  has already been extended with additional code generators for
-  specific HOL constructs. These include datatypes, recursive
-  functions and inductive relations. The code generator for inductive
-  relations can handle expressions of the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{22}{\isachardoublequote}}} is an inductively defined relation. If at
-  least one of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is a dummy pattern ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'',
-  the above expression evaluates to a sequence of possible answers. If
-  all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates
-  to a boolean value.
-
-  The following example demonstrates this for beta-reduction on lambda
-  terms (see also \verb|~~/src/HOL/Proofs/Lambda/Lambda.thy|).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ dB\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Var\ nat\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ App\ dB\ dB\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6465677265653E}{\isasymdegree}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{2}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ Abs\ dB\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ lift\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ k\ then\ Var\ i\ else\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ lift\ s\ k\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ lift\ t\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Abs\ s{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}lift\ s\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}\ i\ then\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ if\ i\ {\isaliteral{3D}{\isacharequal}}\ k\ then\ s\ else\ Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Abs\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{5B}{\isacharbrackleft}}lift\ s\ {\isadigit{0}}\ {\isaliteral{2F}{\isacharslash}}\ k{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{inductive}\isamarkupfalse%
-\ beta\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ beta{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ s{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{2F}{\isacharslash}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ appL{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ appR{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ abs{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Abs\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Abs\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
-\ Test\isanewline
-\isakeyword{contains}\isanewline
-\ \ test{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Var\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ test{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-In the above example, \verb|Test.test1| evaluates to a boolean,
-  whereas \verb|Test.test2| is a lazy sequence whose elements can be
-  inspected separately.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
-\isaantiq
-assert{}%
-\endisaantiq
-\ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ results\ {\isaliteral{3D}{\isacharequal}}\ DSeq{\isaliteral{2E}{\isachardot}}list{\isaliteral{5F}{\isacharunderscore}}of\ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{2}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
-\isaantiq
-assert{}%
-\endisaantiq
-\ {\isaliteral{28}{\isacharparenleft}}length\ results\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\medskip The theory underlying the HOL code generator is described
-  more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
-  illustrate the usage of the code generator can be found e.g.\ in
-  \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Definition by specification \label{sec:hol-specification}%
 }
 \isamarkuptrue%
--- a/etc/isar-keywords.el	Wed Oct 19 16:32:12 2011 +0200
+++ b/etc/isar-keywords.el	Wed Oct 19 16:32:30 2011 +0200
@@ -51,8 +51,6 @@
     "code_deps"
     "code_include"
     "code_instance"
-    "code_library"
-    "code_module"
     "code_modulename"
     "code_monad"
     "code_pred"
@@ -64,7 +62,6 @@
     "coinductive_set"
     "commit"
     "consts"
-    "consts_code"
     "context"
     "corollary"
     "cpodef"
@@ -264,7 +261,6 @@
     "typed_print_translation"
     "typedecl"
     "typedef"
-    "types_code"
     "ultimately"
     "undo"
     "undos_proof"
@@ -292,7 +288,6 @@
     "checking"
     "congs"
     "constrains"
-    "contains"
     "datatypes"
     "defines"
     "file"
@@ -456,8 +451,6 @@
     "code_datatype"
     "code_include"
     "code_instance"
-    "code_library"
-    "code_module"
     "code_modulename"
     "code_monad"
     "code_reflect"
@@ -466,7 +459,6 @@
     "coinductive"
     "coinductive_set"
     "consts"
-    "consts_code"
     "context"
     "datatype"
     "declaration"
@@ -538,7 +530,6 @@
     "type_synonym"
     "typed_print_translation"
     "typedecl"
-    "types_code"
     "use"))
 
 (defconst isar-keywords-theory-script
--- a/src/HOL/Int.thy	Wed Oct 19 16:32:12 2011 +0200
+++ b/src/HOL/Int.thy	Wed Oct 19 16:32:30 2011 +0200
@@ -2390,9 +2390,6 @@
 
 subsection {* Legacy theorems *}
 
-(* used by Tools/Qelim/cooper.ML *)
-lemmas zadd_ac = add_ac [where 'a=int]
-
 lemmas inj_int = inj_of_nat [where 'a=int]
 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
 lemmas int_mult = of_nat_mult [where 'a=int]
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 16:32:12 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 16:32:30 2011 +0200
@@ -74,7 +74,8 @@
 val false_tm = @{cterm "False"};
 val zdvd1_eq = @{thm "zdvd1_eq"};
 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
+val lin_ss =
+  presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]});
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;
--- a/src/Tools/misc_legacy.ML	Wed Oct 19 16:32:12 2011 +0200
+++ b/src/Tools/misc_legacy.ML	Wed Oct 19 16:32:30 2011 +0200
@@ -5,7 +5,6 @@
 
 signature MISC_LEGACY =
 sig
-  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val add_term_names: term * string list -> string list
   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   val add_typ_tfree_names: typ * string list -> string list