src/HOL/SET-Protocol/MessageSET.thy
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-02-13 nipkow 2009-02-13 Moved Nat_Int_Bij into Library
2008-09-02 nipkow 2008-09-02 Replaced Library/NatPair by Nat_Int_Bij.
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.
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2007-12-10 haftmann 2007-12-10 explicit import of theory Main
2007-08-01 wenzelm 2007-08-01 tuned ML bindings (for multithreading); updated timings;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-05-06 haftmann 2007-05-06 dropped legacy ML binding
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2003-10-02 paulson 2003-10-02 removal of junk and improvement of the document
2003-09-23 paulson 2003-09-23 new session HOL-SET-Protocol