SML/NJ compatibility.

Typo.

Deleted old code.

Locale expressions: rename with optional mixfix syntax.

Add back rudely removed and popular -X option.

Now uses File.write and File.append

removed obsolete theorems

use TypedefPcpo for all class instances

log more failure types

added lemmas monofun_lub_fun and cont_lub_fun

put global isatest settings in one file, sourced by the other scripts

Use TypedefPcpo theorem for po instance

use thelub_const lemma

added lemma thelub_const

further tweaks to the SPASS setup

goodby to modUnix

trying to set up portable calling sequences for SPASS and tptp2X

cleaned up select_match do not return trivial matches made simp: t work

Narrower version of the Proof General's head; removal of the alternative icon and environment

Narrower version of the Proof General's head

rewrote continuous isomorphism section, cleaned up

cleaned up, added UU_app and less_funI, removed some obsolete stuff

added defaultsort declaration, moved cpair_less to Cprod.thy

added defaultsort declaration

cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff

removed dependence on Cfun.thy

moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun

new Brouwer ordinal example

more cleanup

tuned thm_style section

added ? explanations

renamed search criterion 'rewrite' to 'simp'

SML/NJ compatibility

new environments for Proof General notes

removed obsolete findI, findE, findEs (and the functions they depended on in Isar/find_theorems)

removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;

*** empty log message ***

grammar

shorted proof that lift is chfin

Removed shell variables. Now uses isatool getenv -b SPASS_HOME.

Generic version of spassshell. Add SPASS_HOME to .bashrc so that shell script can find it.

ML_idf antiquotation

oracle example converted to Isar

cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other

A new structure and reduced indentation

Simplified version of strict sum theory, using TypedefPcpo

Simplified version of strict product theory, using TypedefPcpo

New theory for defining subtypes of pcpos

added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules

Moved admissibility definitions and lemmas to a separate theory

moved continuity simproc to Cfun.thy

moved continuity simproc to Cont.thy

moved theorem cont2cont_CF1L_rev2 to Cont.thy

tuned setsum rewrites

* Pure/Syntax: In schematic variable names, *any* symbol following \<^isub> or \<^isup> is now treated as part of the base name;

interpreters for lfp/gfp added

obsolete;

spassshell and testout.py are used to filter the proof part out of SPASS's output (i.e. cuts out input and search information).

tuned pretty_sg; tuned;

node_trans: revert to original transaction code (pre 1.54);

use: not a theory command!

converted back from 0..< to <.

added email

tuned trace info (depth)

simplifier trace info; Suc-intervals

some adaptions

Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy

tuned;

string FindTheorems.criterion;

added read_criterion/pretty_criterion; improved rule filters -- intro excludes elim rules; tuned output; tuned;

added show_dummy_patterns;

updated;

Retrieve theorems from proof context -- improved version of thms_containing by Rafal Kolanski, NICTA;

added Pure/simplifier.ML, Pure/Isar/find_theorems.ML;

moved everything related to thms_containing to find_theorems.ML; export is_known; added fact_index_of, valid_thms; gen_read': removed unused dummies option; declare_term(_syntax): canonical argument order; removed declare_terms(_syntax);

added reserved;

added ident_with;

fold ProofContext.declare_term;

added 'print_simpset'; tuned 'thms_containing'; removed 'print_intros';

added print_simpset; renamed print_thms_containing to find_theorems; removed print_intros (superceded by find_theorems intro);

added find_theorems.ML, ../simplifier.ML;

tuned terms_of_tpairs;

added string_of_thmref, selections, fact_index_of, valid_thms; moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML; tuned

FindTheorems.print_theorems;

findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;

major tuning;

Simplifier already setup in Pure;

tuned antiquotations;

tuned thms_containing;

tuned;

moved to Pure;

moved here from Provers; removed find_rewrites (superceded by find_theorems rewrite); outer syntax moved to Pure/Isar/isar_syn.ML;

removed find_rewrites (superceded by improved thms_containing);

bug fixes for clause form transformation

converted some problems to Isar format

subst again

Skolemization of simprules and classical rules

pcpo instance for type unit

lucas - bugfix to subst in assumptions: fixed index error for conditional rules.

shortened proof of adm_disj

cleaned up and shortened some proofs

lucas - fixed subst in assumptions to count redexes from left to right.

removed update_node, which is just an instance of map_node; tuned;

tuned;

updated;

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

made para on searching more readable

new cnf function taking Skolemization theorems as an extra argument

consolidation and simplification

documented new thms_containing ('rewrites' still missing)

documented new subst

proper Id line;

updated;

var_or_skolem: always print question mark for vars stemming from skolems;

added read_variable: optional question mark on input; removed obsolete token_assoc; scan_indexname: improved treatment of \<^isub> and \<^isup>; read_var: more robust against bad input; tuned;

substantial tuning -- adapted to common conventions;

re-init ml_prompts after loop termination;

renamed show_var_qmarks to show_question_marks; renamed TermStyle.lookup_style to TermStyle.the_style;

Syntax.read_variable;

renamed show_var_qmarks to show_question_marks; string_of_vname: improved treatment of \<^isub> and \<^isup>;

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