dummy patterns; theory data: copy;

added Isar/comment.ML;

val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;

theory data: copy; consts dummy :: 'a ("'_");

theory data: copy;

improved icons;

Isabelle icons;

patched sum_case;

Obsolete because JDK 1.1.x contains a class ScrollPane

Updated to JDK 1.1.x

Proof mods due to eta contraction during rewriting.

Eta contraction is now performed all the time during rewriting.

currently disabled;

*** empty log message ***

made many specification operators infix

eliminated theory UNITY/Traces

improper simp methods;

tuned;

fold / unfold methods;

tuned;

no Toplevel.print for by, ., ..;

improved print_state;

verbose flag;

use_thy_only made pervasive;

added Isar_examples/NatSum.thy;

Old stuff.

proper quiet_mode; tuned messages;

adapted add_inductive, add_record;

adapted add_inductive;

intrs attributes;

proper quiet_mode;

iff_add_global (from simpdata.ML);

support forward chaining;

tuned;

added Isar_examples/Cantor.ML;

hol_setup, simpdata_setup;

"iff" attribute; simpdata_setup;

hol_setup;

"!" made keyword;

opt_thm_name: name optional;

added oooo;

fixed a bug many years old in rule plusEC

tuned msgs; outer syntax;

tuned;

tuned;

elaborated;

tuned;

tuned antiquotations;

improved 'single' method; added 'contradiction' method;

added thus, hence;

added FINISHED, same_tac;

use /usr/share and /usr/bin;

Now for recdefs that omit the WF relation; removed the separation between draft and theory modes

Now for recdefs that omit the WF relation

Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml

chgrp isabelle;

detailed proofs;

tuned;

oops;

fixed IO;

improved load paths;

single method: include not_elim, imp_elim;

more graceful handling of load paths;

improved auto dir handling;

tuned;

make Isabelle rpm packages for Linux/x86 from the distribution;

use_thy etc.: may specify path prefix, which is temporarily used as load path;

switch_theory: Context.pass;

recdef (TFL) now requires theory Recdef;

recdef requires theory Recdef;

tuned;

rep_datatype syntax: 'induction' instead of 'induct';

add_recdef: actual simpset; add_recdef_x: named simpset;

recdef adapted to RecdefPackage.add_recdef;

Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;

added ex and Modelcheck

tuned;

added for mucke translation;

deleted some old examples in Modelcheck;

added translation from IOA to mucalculus and corresponding modelchecker examples;

moved this trivial example to new ex dir;

changed to include new subdirs ex and Modelcheck;

put types into "" because of signature clash;

added frontend syntax for IOA, moved trivial examples to folder ex;

added modelchecker mucke besides modelchecker eindhoven;

delete old files for adding second modelchecker connection;

$ML_HOME/.arch-n-opsys 2>/dev/null;

smlnj-110 setup made default;

/usr/share/smlnj/bin;

Isamode 2.6 requires patch;

added is_current;

fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;

temporarily fake quiet_mode;

temporarily reverted to 1.24;

IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly) provided HIGHER-ORDER logic

Main is the correct parent

new result extend_LeadsTo

should not refer to Datatype

addition of Kerberos IV example

tidied

improved usage;

loadpath replaced;

and_list;

lifted enum; removed list(1); added and_list(1);

may specify induction predicates as well;

added Isar_examples;

Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

lemmas about proper subset relation;

Proof by induction on types / set / functions.

print_datatypes;

added Tools/induct_method.ML;

'HOL/recdef' theory data;

'HOL/recdef' theory data; induct method setup;

'HOL/inductive' theory data;

Sign.base_name fid;

added incr_indexes, incr_indexes_wrt;

Proof mod.

Added new thms.

quiet_mode;

Tools/inductive_package.ML;