tuned specifications/proofs;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;

renamed Graph.project to Graph.subgraph;

replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts;

renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;

Sorts.minimal_classes;

classes: more direct way to achieve topological sorting; renamed classes to all_classes; added minimal_classes; renamed project to subalgebra, tuned;

replaced classes by all_classes (topologically sorted); added minimal_classes;

replaced Sign.classes by Sign.all_classes (topologically sorted);

Enable new Proof General code again after SML/NJ compatibility fixes by Florian.

Typo in last commit

explicit construction of operational classes

added handling for explicit classrel witnesses

``classes`` now returns classes in topological order

dropped some bookkeeping

simplified class_package

use_ml: reverted to simple output (Poly/ML changed);

removed private files

tuned;

removed nospaces (Char.isSpace does not conform to Isabelle conventions);

tuned msg;

inlined nospaces (from library.ML);

added

some clarifications

different handling of type variable names

added split

fixed misleading error message

dropped section header

added OCaml code generation (without dictionaries)

removed Haskell reserved words

removed Main.thy

moved code generator product setup here

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;

prove hyperpow_realpow using transfer

remove usage of ultra tactic

add lemmas singleton and insert_iff

generalized type of hyperpow; removed hcpow

redefine hSuc as *f* Suc, and move to HyperNat.thy

proper use of IntInf instead of InfInf;

defs/notes: more robust transitivity reasoning;

added trans_terms/props;

locale: print context for begin;

remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq

remove uses of star_n and FreeUltrafilterNat

remove use of FreeUltrafilterNat

added lemmas about hRe, hIm, HComplex; removed all uses of star_n

fixed type

added stub for OCaml serializer

cleanup

whitespace correction

clarifed comment

dropped FIXME comment

clarified character setup

remove references to star_n

SComplex abbreviates Standard

simplified mk/dest_numeral (cf. mk/dest_binum of 1.65); put signature into canonical order;

removed legacy ML bindings;

updated;

tuned signature;

internal_abbrev: observe print mode;

target_abbrev: internal mode for abbrevs; tuned;

edge: actually apply operation!

tuned;

authentic syntax for number_of

introduced mk/dest_numeral/number for mk/dest_binum etc.

fixed syntax for bounded quantification

dropped superfluous header

clarified error message

nat type now has a size functin => no longer needed as special case

simplified

local_abbrev: proper fix/declare of local entities;

Deleted the unused type argument of UVar

tuned comments;