| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
e0d246a1 |
|
29-May-2017 |
eberlm <eberlm@in.tum.de> |
reorganised material on sublists
--HG--
rename : src/HOL/Library/Sublist_Order.thy => src/HOL/Library/Subseq_Order.thy
extra : amend_source : e295fcfca4d0d9db4c5591741cb62b62bb340c87
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
526353aa |
|
07-Jul-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
more instantiations for multiset
|
| #
e746111c |
|
07-Jul-2016 |
blanchet <none@none> |
moved lemmas and locales around (with minor incompatibilities)
|
| #
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;
|
| #
07a7e7cf |
|
13-Mar-2016 |
haftmann <none@none> |
more theorems on orderings
--HG--
extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c
|
| #
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
|
| #
41682711 |
|
19-Jun-2015 |
nipkow <none@none> |
renamed multiset_of -> mset
|
| #
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;
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
5c541a07 |
|
13-Dec-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
077493ab |
|
08-Sep-2010 |
haftmann <none@none> |
modernized primrec
|
| #
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;
|
| #
99b04075 |
|
03-Aug-2007 |
wenzelm <none@none> |
misc cleanup of ML bindings (for multihreading);
|
| #
745db1a3 |
|
26-Jul-2006 |
webertj <none@none> |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
| #
3a22d7a5 |
|
03-Jan-2006 |
paulson <none@none> |
added explicit paths to required theories
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
7ebc34e1 |
|
22-Jul-2004 |
nipkow <none@none> |
Modified \<Sum> syntax a little.
|
| #
2a98d8d4 |
|
15-Jul-2004 |
nipkow <none@none> |
Moved to new m<..<n syntax for set intervals.
|
| #
47b52a8a |
|
11-May-2004 |
obua <none@none> |
changes made due to new Ring_and_Field theory
|
| #
55f6b81a |
|
26-Jan-2004 |
schirmer <none@none> |
* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy
|
| #
b6cc7d2f |
|
15-Jul-2003 |
paulson <none@none> |
tidying
|
| #
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
| #
71fec134 |
|
24-Jan-2003 |
paulson <none@none> |
More conversion of UNITY to Isar new-style theories
|
| #
64484fd5 |
|
05-Mar-2001 |
paulson <none@none> |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|