2006-12-27 haftmann 2006-12-27 moved code generator product setup here
2006-12-27 haftmann 2006-12-27 added code generator test theory
2006-12-27 haftmann 2006-12-27 explizit serialization for Haskell id
2006-12-27 haftmann 2006-12-27 removed code generation stuff belonging to other theories
2006-12-27 haftmann 2006-12-27 moved code generator bool setup here
2006-12-27 haftmann 2006-12-27 exported explicit equality on tokens
2006-12-27 haftmann 2006-12-27 made SML/NJ happy
2006-12-22 paulson 2006-12-22 revised for new make_clauses
2006-12-22 paulson 2006-12-22 tidying the ATP communications
2006-12-22 paulson 2006-12-22 string primtives
2006-12-22 haftmann 2006-12-22 deactivated test for the moment
2006-12-22 paulson 2006-12-22 fixed typo in comment
2006-12-22 ballarin 2006-12-22 Experimenting with interpretations of "definition".
2006-12-21 haftmann 2006-12-21 clarified code
2006-12-21 haftmann 2006-12-21 dropped superfluos code
2006-12-21 haftmann 2006-12-21 code clarifications
2006-12-21 haftmann 2006-12-21 import path made absolute
2006-12-21 haftmann 2006-12-21 added code lemmas for quantification over bounded nats
2006-12-21 aspinall 2006-12-21 Disable new Proof General code until SML/NJ compile fixed.
2006-12-20 aspinall 2006-12-20 Use new Proof General code by default [see comment for reverting]
2006-12-20 paulson 2006-12-20 change from "Array" to "Vector"
2006-12-19 huffman 2006-12-19 add lemmas Standard_starfun(2)_iff
2006-12-19 aspinall 2006-12-19 Missing elements from doc_markup_elements
2006-12-19 aspinall 2006-12-19 Remove obsolete prefixes from error and warning messages.
2006-12-18 haftmann 2006-12-18 added isatool codegen
2006-12-18 haftmann 2006-12-18 dropped CodegenPackage.const_of_idf
2006-12-18 haftmann 2006-12-18 improvements in syntax handling
2006-12-18 haftmann 2006-12-18 added Thyname.* and * constant expressions
2006-12-18 haftmann 2006-12-18 introduces "__" naming policy
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-18 haftmann 2006-12-18 added gen_reflection_tac
2006-12-18 haftmann 2006-12-18 now testing executable content of nearly all HOL
2006-12-18 haftmann 2006-12-18 dropped debug cmd
2006-12-18 haftmann 2006-12-18 explicit nonfix declaration for ML "subset"
2006-12-18 haftmann 2006-12-18 dropped two inline directives
2006-12-18 haftmann 2006-12-18 introduced abstract view on number expressions in hologic.ML
2006-12-18 haftmann 2006-12-18 whitespace fix
2006-12-18 haftmann 2006-12-18 added code generation syntax for some char combinators
2006-12-18 haftmann 2006-12-18 infix syntax for generated code for composition
2006-12-18 haftmann 2006-12-18 new-style oracle setup
2006-12-18 haftmann 2006-12-18 added functions tutorial
2006-12-17 aspinall 2006-12-17 Add abstraction for objtypes and documents.
2006-12-16 huffman 2006-12-16 removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
2006-12-16 huffman 2006-12-16 moved several theorems; rearranged theory dependencies
2006-12-16 huffman 2006-12-16 hypreal_of_hypnat abbreviates more general of_hypnat
2006-12-15 webertj 2006-12-15 tracing instead of warning
2006-12-15 wenzelm 2006-12-15 updated;
2006-12-15 wenzelm 2006-12-15 removed obsolete assert;
2006-12-15 wenzelm 2006-12-15 renamed LocalTheory.assert to affirm;
2006-12-15 wenzelm 2006-12-15 tuned -- accomodate Alice;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-14 huffman 2006-12-14 remove Hyperreal/fuf.ML
2006-12-14 huffman 2006-12-14 remove commented section
2006-12-14 huffman 2006-12-14 remove ultra tactic and redundant FreeUltrafilterNat lemmas
2006-12-14 huffman 2006-12-14 declare insert_iff [simp]
2006-12-14 wenzelm 2006-12-14 activated improved use_ml, which captures output and reports source positions; define use_file in terms of use_ml;
2006-12-14 wenzelm 2006-12-14 tuned;
2006-12-14 huffman 2006-12-14 prove hyperpow_realpow using transfer
2006-12-14 huffman 2006-12-14 remove usage of ultra tactic
2006-12-14 huffman 2006-12-14 add lemmas singleton and insert_iff