added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)

version update

include x86_64

make symlink handling compatible with whitespaces

sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances); keep legacy stuff separate; tuned;

added plain_prop_of;

added smart_conjunction_tac, prove_multi, prove_multi_standard;

auto update

fixed treatment of higher-order simprules

*** empty log message ***

more on rev

intersection

more about list_update

some more lemmas about multiset_of

sped up a bit

removed --version which is not a valid polyml flag and has no effect

make symlink handling compatible with whitespaces

minor tidying

removed unnecessary (?) check

tidied

partial modernising of theory headers

bug in plusinf and mininf for the oracle fixed.

reverted last change (dependencies in HOL)

Added binder syntax for fix

removed -a option; fixed -d option to do what -a was trying; tuned;

lucas - updated to reflect isand.ML update

lucas - improved comments, clarified function behaviour, added missing functions for working with meta variables.

export intro_classes_tac;

allow symlinks to all proper Isabelle executables; isabelle-process: Poly/ML no longer needs Perl to run an interactive session;

eval command line: show results; tuned;

no longer need feeder to run normal interactive sessions;

tuned;

restored AUTO_BASH/PERL -- beware of ./configure! rm -f generated files to avoid accidental overwriting symlinked targets;

restored AUTO_BASH/PERL -- beware of ./configure!

reverted accidental commit of user modification;

ALL_LOGICS: topological order;

improved handling of symlinks; ALL_LOGICS: topological order; removed remains of deceased -p option; reverted accidental commit of user modification;

improved handling of symlinks;

eta-expanded a function

HTML standard conformity: done

test sml/nj devel only for the moment

Fixed bug in fact activation.

*** empty log message ***

Subsumption of locale interpretations.

tuned comment;

added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);

SynExt.standard_token_markers

removed token_trans.ML (some content moved to syn_ext.ML);

eval command line arguments; tuned;

qualified name Pure.skip_proof;

added structure Isar (from isar.ML);

removed structure PureIsar;

qualified name Pure.attribute;

removed isar.ML; removed structure PureIsar;

improved read_tyname; merge_stamps, merge_refs: error instead of raise TERM;

added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;

tuned proofs;

removed Pure/Syntax/token_trans.ML Pure/Thy/ROOT.ML Pure/Proof/ROOT.ML Pure/Isar/isar.ML;

_gt, _gt: syntax instead of consts;

cover CPure.- and CPure._ as well;

content moved to outer_syntax.ML;

content moved to Pure/ROOT.ML;

removed obsolete xterm token translations;

removed last occurrences of OS.Process.sleep

x-symbol syntax

tidied

lucas - fixed a big with renaming of bound variables. Other small changes.

run smlnj devel on sunbroy2 and stable on atbroy51 until faster machines are around

added PG hang to FAQ

tuned

howto for changing web pages, simplified makefile access

check in Isabelle2004 versions to make web page changes easier

updated, added Admin/page after-release maintenance

wakeonlan for macbroy33

test stable and devel version of smlnj

adapt theories and ML files to new CPure/Pure arrangement;

The CPure theory -- Pure with alternative application syntax.

The Pure theory.

removed;

superceded by Pure.thy and CPure.thy;

adapt theories and ML files to new CPure/Pure arrangement;

Adapted use command to new behaviour of Toplevel.node_trans

Adapted to new interface of instantiation and unification / matching functions.

- Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.

Moved cterm_fun from Thm to Drule.

Modified variable index in proof (necessary due to changes in the kernel).

Adapted to new interface of instantiation and unification / matching functions.

Made inst1_tac more robust against changes of variable indices.

fix

tuning locales

removed tracing info

added hearder lines and deleted some redundant material

adding the Proof General preview

improved SML/NJ compatibility, etc.

Added op in front of constructor for better parsing.

Fix automatic determination of poly version.

removed redundant readlink call

call to Array.modifyi replaced

Corrected the problem with the ATP directory.

Used locale interpretations everywhere. -> lemma had new name

Used locale interpretations everywhere.

Removed remaining references to Main.thy in reconstruction code.

Allow symlinks to shell scripts

added locale instantiation

refute extended

syntax fix

more tidying of libraries in Reconstruction

Completed integration of reconstruction code. Now finds and displays proofs when used with modified version of Proof General. C.Q.

auto update

restored the target HOL-Complex-Import

fixed presentation

Removed mult_commute axiom from comm_semiring axclass.

compilation error fixed

support for recursion over mutually recursive IDTs

Cleaned up, now use interpretation.

Cleaned up, now uses interpretation.

deleted obsolete code

Interpretation supports statically scoped attributes; documentation.

updated;

added delete_safe, insert, remove, remove_multi; tuned;