try chown root:root;

renamed 'dummy' to 'dummy_pattern' (less dangerous);

tuned;

method = meth3 (again);

peoper defer_recdef interface;

theory data: copy;

separated recdef / defer_recdef;

tuned defer_recdef interfaces;

comment, interest;

Comment.text;

comment sections; made "%" a keyword;

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;