doc-src/TutorialI/Protocol/Message.thy
2010-02-11 wenzelm 2010-02-11 modernized syntax/translations;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-28 haftmann 2009-07-28 reinserted legacy ML function
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-16 wenzelm 2009-03-16 updated generated file;
2009-03-13 wenzelm 2009-03-13 more regular method setup via SIMPLE_METHOD;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 eliminated OldGoals.inst;
2008-06-11 wenzelm 2008-06-11 OldGoals.inst;
2008-06-11 wenzelm 2008-06-11 RuleInsts.res_inst_tac with proper context;
2008-05-07 berghofe 2008-05-07 Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.
2007-11-08 nipkow 2007-11-08 fix
2007-07-23 berghofe 2007-07-23 Tuned.
2007-07-23 berghofe 2007-07-23 LaTeX code is now generated directly from theory files.
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-09-01 paulson 2003-09-01 Corrections due to John Matthews
2001-04-11 paulson 2001-04-11 symlinks to ../../../HOL/Auth. Fingers crossed...