#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
3f40ae52 |
|
05-Jul-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
instantiate multiset with multiset ordering
|
#
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
10f473d6 |
|
26-Feb-2016 |
haftmann <none@none> |
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
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
bf759ce8 |
|
10-Jun-2015 |
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Renaming multiset operators < ~> <#,...
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
03184bca |
|
22-Mar-2014 |
haftmann <none@none> |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
#
f3bdee62 |
|
25-Dec-2013 |
haftmann <none@none> |
prefer abstract simp rule
|
#
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
f152d60b |
|
22-Feb-2010 |
haftmann <none@none> |
tuned proofs
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
3bc8e14e |
|
21-Sep-2009 |
haftmann <none@none> |
tuned proof; tuned headers
|
#
d6c6c9ba |
|
08-Dec-2006 |
paulson <none@none> |
patched up the proofs agsin
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
da2ac1c7 |
|
03-Aug-2004 |
paulson <none@none> |
new simprules Int_subset_iff and Un_subset_iff
|
#
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
#
2380b71a |
|
04-Feb-2003 |
paulson <none@none> |
some x-symbols
|
#
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
#
06317d69 |
|
30-Jan-2003 |
paulson <none@none> |
converting more UNITY theories to new-style
|
#
64f90b13 |
|
18-Oct-2000 |
wenzelm <none@none> |
use Multiset from HOL/Library;
|
#
2f0a85ab |
|
02-Jun-2000 |
paulson <none@none> |
new parent MultisetOrder and new results about multiset unions
|
#
ee8f28f8 |
|
24-May-2000 |
paulson <none@none> |
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
|
#
07f81ce6 |
|
13-Jan-2000 |
paulson <none@none> |
still working; a bit of polishing
|
#
808483ad |
|
13-Jan-2000 |
paulson <none@none> |
working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.
|
#
34f55c37 |
|
22-Dec-1999 |
paulson <none@none> |
Working version after a FAILED attempt to base Follows upon LeadsETo
|
#
ac58ad4b |
|
10-Jun-1999 |
paulson <none@none> |
shortened Follows to Fols
|
#
294e5853 |
|
24-May-1999 |
paulson <none@none> |
Theory of the "Follows" relation
|