renamed show_var_qmarks to show_question_marks; var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;

updated;

renamed show_var_qmarks to show_question_marks;

removed ISAMODE settings;

no longer support isa-FOO interface; removed Isamode; tuned;

no longer support isa-FOO interface;

tuned;

obsolete;

added comment

streamlined proof using new subst method

moved credit to CONTRIBUTORS;

moved credit to CONTRIBUTORS; tuned;

tuned;

export ISABELLE_HOME, do not normalize; tuned;

removed THIS_IS_ISABELLE_ADMIN;

removed rev_append; tuned presentation of datatype option: removed apsome, export the and if_none;

obsolete;

added;

proper treatment of directory links; tuned;

use Drule.vars_of_terms

Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ

searching for thms by combination of criteria (intro, elim, dest, name, term pattern)

export parser for "-"

line wrap

Eta-expanded merge function (to make SmlNJ happy).

added Proof.context to antiquotation

lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)

-(n::nat) is now regarded as atomic

Bugfix in syntax translation for record type.

theorem names for caching

memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule

first-order now ignores "all"

fixed a few things and added Haftmann as author

documented new subst method

corrections

Added thms by Brian Huffmann

new cterm primitives

oops...cannot use subst here

table centering, headline 'other platform'

unfolding of Ex1

choice_const moved to hologic.ML

from simplesubst to new subst

minor corrections

made file links local, smoothed text over in some places

made file list nicer

moved description (dist area) out of link

made download links local, provide explicit list of files to download

shortened

MAILTO: makarius@sketis.net

lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule

added notes for mac os

Added notes for installation on Windows

added option 'tidy=' to makefile, for optional processing of results by HTML tidy

replaced some outdated HTML by more modern constructs

added new antiquotations

Replaced all unnecessary uses of SOME with THE or LEAST

lucas - added option to select occurance to rewrite e.g. (occ 4)

lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.

lucas - added update node function.

Added eta_long attribute.

Added eta_long_conversion.

eta-expansion

fixed lin.arith

neqE applies even if the type is not one which partakes in linear arithmetic. This lead to confusion. Now there are multiple type specific neqE.

Fixing a problem with lin.arith.

make mkdir usable with cygwin

Replaced reference to SPASS with general one - set SPASS_HOME in settings file. Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.

final implementation of antiquotations styles

Added short description of thm_style and term_style antiquotation

*** empty log message ***

lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.

lucas - added dest_TVar and dest_TFree.

Removed nodup_vars avoiding hack

fixed

turned 2 lemmas into simp rules

*** empty log message ***

fixed setsum problem

meta-logic connectives now forbidden

deleted redundant code

fixed reference to top-level

introduced @{const ...} antiquotation

introduced @{const ...} antiquotation

added to isatest-doc MAILTO

added myself to mailing list

superceded by IsarOverview

fixed typo

separate test run for theories in Doc/

use absolute path to find LaTeXSugar and OptionalSugar

export DISTPREFIX to devel page Makefile

fixed dependencies

don't leave stale root.pdf / root.dvi

move generated files to document/ to avoid CVS file overwrite in generated/ cleanup (no generated root.pdf, session_graph.pdf etc)

move generated files to document/, avoid CVS file overwrite in generated/

unused

removed obsolete exercise collection (is now in coursematerial)

updated PG preview for new thms-containing

better error reporting

put 8h time limit on test

move isadist to ~/tmp/

publish only *.html

include new thms_containing

credits

new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)

new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)

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

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;

clarified insert/remove; tuned canonical fold/fold_rev;

tuned;

binds/thms: do not store options, but delete from table; tuned;

tuned comments;

removed;

expect translations functions to be stamped already; added remove_const_gram;

added stamp_trfun, mk_trfun, eq_trfun;

tuned extend_prtabs; added remove_prtabs;

added make_gram; merge_gram: do not add chain productions to prods;

identify binder translations only once (admits remove);

Syntax.mk_trfun;

tuned (t)inst_tab_elem;

added 'no_syntax' command;

added del_modesyntax(_i);

added del_modesyntax(_i); added print_all_data;