added code generator test theory

explizit serialization for Haskell id

removed code generation stuff belonging to other theories

moved code generator bool setup here

exported explicit equality on tokens

made SML/NJ happy

revised for new make_clauses

tidying the ATP communications

string primtives

deactivated test for the moment

fixed typo in comment

Experimenting with interpretations of "definition".

clarified code

dropped superfluos code

code clarifications

import path made absolute

added code lemmas for quantification over bounded nats

Disable new Proof General code until SML/NJ compile fixed.

Use new Proof General code by default [see comment for reverting]

change from "Array" to "Vector"

add lemmas Standard_starfun(2)_iff

Missing elements from doc_markup_elements

Remove obsolete prefixes from error and warning messages.

added isatool codegen

dropped CodegenPackage.const_of_idf

improvements in syntax handling

added Thyname.* and * constant expressions

introduces "__" naming policy

switched argument order in *.syntax lifters

added gen_reflection_tac

now testing executable content of nearly all HOL

dropped debug cmd

explicit nonfix declaration for ML "subset"

dropped two inline directives

introduced abstract view on number expressions in hologic.ML

whitespace fix

added code generation syntax for some char combinators

infix syntax for generated code for composition

new-style oracle setup

added functions tutorial

Add abstraction for objtypes and documents.

removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy

moved several theorems; rearranged theory dependencies

hypreal_of_hypnat abbreviates more general of_hypnat

tracing instead of warning

updated;

removed obsolete assert;

renamed LocalTheory.assert to affirm;

tuned -- accomodate Alice;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

remove Hyperreal/fuf.ML

remove commented section

remove ultra tactic and redundant FreeUltrafilterNat lemmas

declare insert_iff [simp]

activated improved use_ml, which captures output and reports source positions; define use_file in terms of use_ml;

tuned;