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;

triple_swap;

Wrapper module for Konrad Slind's TFL package.

remoced old set_current_thy;

tuned messages;

intrs: names and atts;

tuned comments; tuned types;

tuned comments; intrs: names and atts; Isar outer syntax;

tuned comments;

intrs: provide names and atts;

cleaned comments;

tuned;

fixed named type infixes (actual BUG!);

updated isatool install;

-p option; -k option;

adapted isatool install;

improved isatool install;

tuned;

ML_PLATFORM;

ML_PLATFORM;

fixed @@;

fixed bib file

fixed;

new definition for nth. added warnings, if primrec definition is deleted from simpset.

useless relic

arith_tac

tuned;

common qed and end of proofs;

* New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

New bounded quantifier syntax: !x<i. P etc

added new theory Yahalom_Bad

added new theory Yahalom_Bad

exchanged the order of Gets and Notes in datatype event

fixed thm_name again;