src/HOL/UNITY/Follows.thy
24 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-07-05 fleury 2016-07-05 instantiate multiset with multiset ordering
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-02-26 haftmann 2016-02-26 more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-06-10 Mathias Fleury 2015-06-10 Renaming multiset operators < ~> <#,...
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2013-12-25 haftmann 2013-12-25 prefer abstract simp rule
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-22 haftmann 2010-02-22 tuned proofs
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-21 haftmann 2009-09-21 tuned proof; tuned headers
2006-12-08 paulson 2006-12-08 patched up the proofs agsin
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-02-04 paulson 2003-02-04 some x-symbols
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style
2000-10-18 wenzelm 2000-10-18 use Multiset from HOL/Library;
2000-06-02 paulson 2000-06-02 new parent MultisetOrder and new results about multiset unions
2000-05-24 paulson 2000-05-24 restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
2000-01-14 paulson 2000-01-14 still working; a bit of polishing
2000-01-13 paulson 2000-01-13 working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.
1999-12-22 paulson 1999-12-22 Working version after a FAILED attempt to base Follows upon LeadsETo
1999-06-10 paulson 1999-06-10 shortened Follows to Fols
1999-05-24 paulson 1999-05-24 Theory of the "Follows" relation