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