fixed WWW links

Three new facts about Image

Replaced \\1 by $1 as Perl itself asked me to...

Fixed the description of recdef

tuned msgs;

improved tracing of rewrite rule application;

removed dead messy code;

added read_var;

tuned;

Updated MOD reference

added symbols syntax;

reorganized into individual theories;

tuned;

make images;

tuned URL;

polyml-3.1;

obsolete;

added thms wrt weakening and strengthening in Abstraction;

New Jersey inactive;

HOL/record;

error with instantiantion of sub-records removed

added record.ML;

tuned;

added unit and prod stuff;

fixed Id;

smlnj-110 factory default;

added of_sort;

added base_path;

added simulations files to IOA;

added forward simulation correectness;

Simplification: sel make and update make

added abstraction files;

added further IOA liles;

updated to Isabelle98;

tuned;

added files containing temproal logic and abstraction;

Delsimprocs nat_cancel;

tuned;

Tidying, mostly to do with handling a more specific version of Fake_parts_insert

tuned;

tuned;

fixed author;

Simplified proofs by omitting PA = {|XA, ...|} from RA2

trivial tidy

tuned;

automatic index.html patch;

tuned;

tuned ISABELLE_TMP_PREFIX;

thm_ord;

eliminated make_ord;

ISABELLE_TMP_PREFIX: $LOGNAME

several minor updates;

tuned;

index.html for Isabelle Distribution Area;

updated to Isabelle98;

tuned;

fixed thm_less;

Expressed most Oops rules using Notes instead of Says, and other tidying

added split_paired_Ex to the implicit simpset

added select_equality to the implicit claset

added select_equality to the implicit claset added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset removed split_select renamed Collect_Prod to Collect_split

added newline at end of file

*** empty log message ***

streamlined specification of included theories

corrected Title

removed obsolete comment

added Univalent

removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses

added update_same, update_other, update_triv, and map_of_SomeD

replaced fn _ => by K

*** empty log message ***

New rule: image_subset

Restored the ciphertext in OR4 in order to make the spec closer to that in OtwayRees.thy

Tidied by adding more default simprules

adapted to new split order;

adapted to new sort function;

improved targets; fixed dependencies on parent logics;

tuned;

added -u option (again);

Now calls Blast_tac more often

obsolete;

feeder;

Changed required by new blast_tac (the one that squashes flex-flex pairs)

Blast_tac now squashes flex-flex pairs immediately

New theorem image_subsetI

Making proofs faster, especially using keysFor_parts_insert

do require perl;

Auto_tac now has type tactic, not unit->tactic

Declared startTiming and endTiming

use feeder to pipe into ML; cleaned up;

removed -i option;

nth -> !

nth -> !

feed isabelle session;

commented out symboloutput.pl;

added feeder.pl;

pretty_name_space;

removed declared; improved dest;

removed distinct_fst_string;

improved error handling;

fixed execute;

made MLWorks happy;

stderr to $LOG;

Symtab.empty;

improved internal representation;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP;

renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;

renamed Symtab.null to Symtab.empty;

added >> : (theory -> theory) -> unit;

tuned;

replaced symtab.ML by table.ML;

renamed (is_)null to (is_)empty; renamed DUPLICATE to DUP; renamed extend_new to extend;

Generic tables (lacking delete operation). Implemented as 2-3 trees.

tuned;

export range_type;

improved comment;

More restrictive patterns to prevent changing comments

New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

Tidied using rev_iffD1

Now Blast_tac works properly

Tidied. Also better proof using new blast_tac

Decremented subscript because of change to iffD1

Tidied using rev_iffD1, etc

Tidied using rev_iffD1

Tidied using more default rules

Overloading info for image

tidied

New rules rev_iffD{1,2}

Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac

New "obvious theorems"

Added range-type for completeness

New example

New rules rev_iffD{1,2}

corrected removal to /tmp/tmp.c

added removal to /tmp/tmp.txt

records without signature

remove signatrue from records

tuned;

new version;

added record.ML;

first version of records

pasted old insertion sort (does not work with new sort function!)

adapted to new sort function;

log file; elapsed time;

leading 0s;

tuned;

adapted to new sort function;

log files; 'clean' target;

tuned;

added rev_order, make_ord; reimplemented sort function: stable version of quicksort;

term order; signature;

term order stuff moved to term.ML;

log file; elapsed time;

'clean' target;

adapted to new sort function;

Term.termless;

adapted to new sort function;

removed maketest;

showtime - print time.

added expand_split_asm

UNIV_I no longer counts as safe

tuned;

added mlworks;

added MLWorks;

misc improvements; stack_overflow_handler;

tuned tmp file name;

tuned comment;

added ML-Systems/mlworks.ML;

MLWorks startup script (for 1.0r2 or later).

renamed to mlworks.ML;

Compatibility file for MLWorks version 1.0r2 or later.

expandshort;

Simplified proofs using rewrites for f``A where f is injective

Simplified SpyKeys and ClientKeyExch as suggested by James Margetson

obsolete;

tuned;

obsolete;

adapted from Larry's version;

improved;

improved COMMIT_RO;

tuned;

polyml-3.1;

make smlnj-110 default;

tuned;

tuned;

No longer depend on theory context!

version = "Isabelle98: Jan 1998";

tuned comment;

smlnj-110;

deleted smlnj-1.09.ML;

obsolete;

Compatibility file for Standard ML of New Jersey.

tuned;

prepared for Isabelle98;

added;

obsolete;

tuned;

tuned msg;

tuned;

major update;

SYNC;

new blast_tac no longer works here

More deterministic (?) contr_tac

More deterministic and therefore faster (sometimes) proof reconstruction

ugly patch for new Blast_tac

Faster proof of mult_less_cancel2

tuned;

Tidied final proof

Tidied proof of finite_subset_induct

Got rid of mod2_neq_0

\subsection{*Theory inclusion};

Tidying to fix overfull lines, etc

Comprehensive (??) list of bugs, fixed or not

tuned;

added print_claset;

Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).

Got rid of some preds and replaced some n~=0 by 0<n.

Cleaned up arithmetic mess.

instantiate';

changed typed_print_translation;

tuned;

nat_cancel enabled by default;

adapted proofs to cope with simprocs nat_cancel;

improved arbitrary_def: we now really don't know nothing about it!

use_thy no longer requires writable current directory;

adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);

simplification procedures nat_cancel enabled by default;

tmp_name;

added print_simpset;

added is_base;

added reset_context;

added eq_set;

moved global_names ref to Pure/ROOT.ML;

pred -> -1

pred n -> n-1

Simplified proofs.

Added thm mult_div_cancel

n ~= 0 should become 0 < n

Replaced n ~= 0 by 0 < n

pass return code!!

Fixed the treatment of substitution for equations, restricting occurrences of variables on the RHS. Improves performance in many cases, though a few old proofs fail

updated for latest Blast_tac, which treats equality differently

Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML

Tidying and some comments

updated for latest Blast_tac, which treats equality differently

Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic

updated for latest Blast_tac, which fixes an equality bug

Miniscoping now used except for one proof

adapted to new term order;

tuned term order; added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;

tuned trfuns types;

added prod_ord, dict_ord, list_ord;

File.tmp_name;

added tmp_name;

ISABELLE_TMP;

added context.ML;

Global contexts: session and theory.

added Thy/context.ML;

open;

nat_cancel simprocs;

ISABELLE_TMP_PREFIX;

ISABELLE_TMP;

Added DiffCancelSums.

New guarantee B_trusts_NS5, and tidying

speed-up

args for record data

Removed "open Mutil;"

Added comments

New timing functions startTiming and endTiming

addsplits now in FOL, ZF too

New example

Printing of statistics including time for search & reconstruction

New example

Removed dead code.

Moved the quantifier elimination simp procs into Provers.

Quantifier elimination procs.

Fixed the definition of `termord': is now antisymmetric.

several minor updates;

SYNC;

removed read_cterms;

fixed warning;

removed same_thm;

Tidying, mostly indentation

Deleted some needless addSIs; got rid of a slow Blast_tac

mk_norm_sum;

separate lists of simprocs;

Added rule impCE'

Blast_tac can prove Pelletier\'s problem 46\!

Tidying and using equalityCE instead of the slower equalityE

The change from iffE to iffCE means fewer case splits in most cases. Very few proofs are affected, almost none adversely

Tidying

Tidying and modification to cope with iffCE

Added rule impCE'

Changes to AddIs improve performance of Blast_tac

Statistics

updated comment

Tidying and modification to cope with iffCE

added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;

added Arith provers;

Setup various arithmetic proof procedures.

added dest_nat;

moved to Arith/;

Cancel common constant factor from balanced exression.

Cancel common summands of balanced expressions.

removed conv_prover;

tuned;

added crep_cterm;

fixed type of thms_containing;

added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a; added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;

cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;

removed merge_opts;

managed merge details;

resolved merge conflict;

Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.

fixed warning;

made SML/NJ happy;

tuned;

replaced by seq.ML;

changed Pure/Sequence interface;

SYNC;

cd, use: path variables;

comment;

obsolete;

changed Pure/Sequence interface -- isatool fixseq;

changed Sequence interface (now Seq, in seq.ML);

cd, use etc. now support path variables; changed Pure/Sequence interface;

fix references to obsolete Pure/Sequence structure;

tidying

analz_mono_contra_tac was wrong

Deleted some useless comments

minor improvements of formulation and proofs

corrected INDUCT_FILES

$ISABELLE_HOME/src;

improved error msg;

removed old note;

adapted print methods;

improved theorems print method: transfer_sg;

init_data: improved print method;

removed data.ML (made part of sign.ML);

added type object = exn;

added transfer_sg;

fixed xstr token encoding;

tuned infer_types interface;

tuned infer_types interface;

moved Sign.print_sg to display.ML;

exported pretty_classrel, pretty_arity; added infer_types_simult; tuned infer_types interface; moved print_sg to display.ML;

added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; added multiply: 'a list * 'a list list -> 'a list list;

added implode_xstr: string list -> string, explode_xstr: string -> string list;

Now uses induct_tac

Updated the NatSum example

New, higher-level definition of \\out macro

Speeded up the proof of succ_lt_induct_lemma

Two new rewrites

Got rid of some slow deepen_tac calls

Renamed "overload" to "overloaded" for sml/nj compatibility

No more makeatletter/other

Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys

The dtac was discarding information, though apparently no proofs were hurt

Fixed bug in inst_split.

improved big_rec_name lookup;

Updated comments. A bug causes MLWorks to use much more storage than necessary

Rationalized error handling: if low-level tactic (depth_tac) cannot accept the goal then it raises exception TRANS. Top-level tactics (blast_tac) generate warnings and then fail immediately.

Tuned function mk_cntxt_splitthm. Fixed bug which caused split_tac to fail when (Const ("splitconst", ...) $ ...) was of function type.

Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.

Redesigned the decision procedures for (Abelian) groups and commutative rings.

Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"

merge_refs: check for different versions of theories;

export read_raw_typ;

fixed record parser;

improved record syntax;

made SML/NJ happy;

added thin_refl to hyp_subst_tac

refer to $ISABELLE_HOME/src;

structure BasisLibrary;

renamed to use.ML;

Redefine 'use' command in order to support path variable expansion, automatic suffix generation, and symbolic input filtering (if required).

adapted to new Use, File structs;

added path variables;

File system operations.

moved old file stuff from library.ML to Thy/browser_info.ML; subdir_of no longer infix;

added file.ML, use.ML; removed symbol_input.ML;

tuned warning msg;

major cleanup; removed several obsolete functions; moved file stuff to Thy/file.ML;

moved 'latex' from library.ML to goals.ML;

tuned prths;

structure BasisLibrary;

added Thy/file.ML, Thy/use.ML; removed Thy/symbol_input.ML;

renamed split_prem_tac to split_asm_tac

restored last version

simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm cladata.ML: unintentinally committed

renamed split_T_case_prem to split_T_case_asm

renamed split_prem_tac to split_asm_tac

renamed split_prem_tac to split_asm_tac split_asm_tac: simplification, debugged first_prem_is_disj

Fixed indentation

Rationalized the theorem if_image_distrib. Added parens to not_empty.

Fixed indentation

Fixed spelling error

Made some proofs more robust

Now applies "map negOfGoal" to lits when expanding haz rules. Also improved comments

ASCII-fied;

polished definition of find_index_eq

check files for non-ASCII characters;

replaced 8bit characters

fixed LAM<...> syntax;

fixed spelling;

added split_prem_tac

changed libraray function find to find_index_eq, currying it

added contrapos

added contrapos2

added exists_Const

Each datatype t now proves a theorem split_t_case_prem P(t_case f1 ... fn x) = (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | ... (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) ) )

Perl no longer optional;

deriv: eliminated references to theory;

tuned;

tuned;

hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function

subgoal_tac displays a warning if the new subgoal has type variables

mkdir -p bin;

Tools/8bit: ./mk;

*** empty log message ***

tuned;

abandoned generation of tmp files

various improvements

reflecting changes of isa2latex

several minor improvements

added ax2isa

added ax2isa

added isabelle14 and isabelle24

removed gererated files

added entry for manual

*** empty log message ***

Now introduces Safe_tac

Ran expandshort, especially to introduce Safe_tac

Adapted to removal of UN1_I, etc

Adapted to removal of UN1_I, etc

UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves

Expandshort; new theorem le_square

generalized UNION1 to UNION

Tidied Key_supply3

fixed comment

UNIV & UNION1

Ran expandshort, especially to introduce Safe_tac

Ran expandshort, especially to introduce Safe_tac

adapted typed_print_translation;

tuned record_info;

fixed exception OPTION;

adapted pure_trfunsT; added type_tr/tr'; eliminated mk_ofclassS_tr';

print translation: added show_sorts argument;

adapted syn_ext_trfunsT;

adapted extend_trfunsT;

fixed exception OPTION;

added TYPE syntax; tuned;

fixed exception OPTION;

adapted add_trfunsT; defs: admit TYPE arguments;

adapted add_trfunsT;

fixed exception OPTION; added try, can;

base root = "";

Added an alternativ version of AutoChopper and a theory for the conversion of automata into regular sets.

removed redundant ball_image added image_cong and not_empty added ball and bex of UNIV

removed redundant ball_empty and bex_empty (see equalities.ML)

added several theorems

added the, option_map, and case analysis theorems

added zip and nodup

added theorems for Eps

tuned usage;

HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;

tuned to make non-Poly/MLs happy;

tuned 'records' stuff;

added pretty_ctyp;

tuned;

type object = exn (enhance readability);

*** empty log message ***

* removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)

simplified (and corrected) syntax definition of fapp

data kinds 'datatypes', data kinds 'records' added

removed old datatype_info;

added Thy/path.ML;

Logic.loops -> Logic.rewrite_rule_ok

logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.

added path.ML;