1999-04-27 wenzelm 1999-04-27 verbose flag;
1999-04-27 wenzelm 1999-04-27 use_thy_only made pervasive;
1999-04-27 wenzelm 1999-04-27 added Isar_examples/NatSum.thy;
1999-04-27 nipkow 1999-04-27 Old stuff.
1999-04-27 wenzelm 1999-04-27 proper quiet_mode; tuned messages;
1999-04-27 wenzelm 1999-04-27 adapted add_inductive, add_record;
1999-04-27 wenzelm 1999-04-27 adapted add_inductive;
1999-04-27 wenzelm 1999-04-27 intrs attributes;
1999-04-27 wenzelm 1999-04-27 proper quiet_mode;
1999-04-27 wenzelm 1999-04-27 iff_add_global (from simpdata.ML);
1999-04-27 wenzelm 1999-04-27 support forward chaining;
1999-04-27 wenzelm 1999-04-27 tuned;
1999-04-27 wenzelm 1999-04-27 added Isar_examples/Cantor.ML;
1999-04-27 wenzelm 1999-04-27 hol_setup, simpdata_setup;
1999-04-27 wenzelm 1999-04-27 "iff" attribute; simpdata_setup;
1999-04-27 wenzelm 1999-04-27 hol_setup;
1999-04-27 wenzelm 1999-04-27 "!" made keyword;
1999-04-27 wenzelm 1999-04-27 opt_thm_name: name optional;
1999-04-27 wenzelm 1999-04-27 added oooo;
1999-04-26 paulson 1999-04-26 fixed a bug many years old in rule plusEC
1999-04-26 wenzelm 1999-04-26 tuned msgs; outer syntax;
1999-04-23 wenzelm 1999-04-23 tuned;
1999-04-23 wenzelm 1999-04-23 tuned;
1999-04-23 wenzelm 1999-04-23 elaborated;
1999-04-23 wenzelm 1999-04-23 tuned;
1999-04-23 wenzelm 1999-04-23 tuned antiquotations;
1999-04-23 wenzelm 1999-04-23 improved 'single' method; added 'contradiction' method;
1999-04-23 wenzelm 1999-04-23 added thus, hence;
1999-04-23 wenzelm 1999-04-23 added FINISHED, same_tac;
1999-04-23 wenzelm 1999-04-23 use /usr/share and /usr/bin;
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation; removed the separation between draft and theory modes
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation
1999-04-23 paulson 1999-04-23 Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
1999-04-23 wenzelm 1999-04-23 chgrp isabelle;
1999-04-23 wenzelm 1999-04-23 detailed proofs;
1999-04-23 wenzelm 1999-04-23 tuned;
1999-04-23 wenzelm 1999-04-23 oops;
1999-04-22 wenzelm 1999-04-22 fixed IO;
1999-04-22 wenzelm 1999-04-22 improved load paths;
1999-04-22 wenzelm 1999-04-22 single method: include not_elim, imp_elim;
1999-04-22 wenzelm 1999-04-22 more graceful handling of load paths;
1999-04-22 wenzelm 1999-04-22 improved auto dir handling;
1999-04-22 wenzelm 1999-04-22 tuned;
1999-04-22 wenzelm 1999-04-22 make Isabelle rpm packages for Linux/x86 from the distribution;
1999-04-22 wenzelm 1999-04-22 use_thy etc.: may specify path prefix, which is temporarily used as load path;
1999-04-22 wenzelm 1999-04-22 switch_theory: Context.pass;
1999-04-22 wenzelm 1999-04-22 recdef (TFL) now requires theory Recdef;
1999-04-22 wenzelm 1999-04-22 recdef requires theory Recdef;
1999-04-22 wenzelm 1999-04-22 tuned;
1999-04-22 wenzelm 1999-04-22 rep_datatype syntax: 'induction' instead of 'induct';
1999-04-22 wenzelm 1999-04-22 add_recdef: actual simpset; add_recdef_x: named simpset;
1999-04-22 wenzelm 1999-04-22 recdef adapted to RecdefPackage.add_recdef;
1999-04-22 wenzelm 1999-04-22 Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;
1999-04-22 mueller 1999-04-22 added ex and Modelcheck
1999-04-22 wenzelm 1999-04-22 tuned;
1999-04-22 mueller 1999-04-22 added for mucke translation;
1999-04-22 mueller 1999-04-22 deleted some old examples in Modelcheck;
1999-04-22 mueller 1999-04-22 added translation from IOA to mucalculus and corresponding modelchecker examples;
1999-04-22 mueller 1999-04-22 moved this trivial example to new ex dir;
1999-04-22 mueller 1999-04-22 changed to include new subdirs ex and Modelcheck;