| #
551b6192 |
|
05-Mar-2019 |
haftmann <none@none> |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
| #
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
| #
09859749 |
|
18-Nov-2018 |
haftmann <none@none> |
removed legacy input syntax
|
| #
888b6a7c |
|
12-Sep-2018 |
nipkow <none@none> |
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
|
| #
69def9ca |
|
26-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
--HG--
extra : amend_source : fa78190ac2ee02ba33d22a4ee58362bc893ff097
|
| #
965df47d |
|
12-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Changes to complete distributive lattices due to Viorel Preoteasa
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
4ed5daad |
|
04-Nov-2017 |
wenzelm <none@none> |
prefer main entry points of HOL;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
| #
94ea3a82 |
|
06-Jul-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
| #
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
| #
2cc0ca92 |
|
07-Sep-2012 |
haftmann <none@none> |
lattice instances for option type
|
| #
69e75063 |
|
13-Jul-2011 |
haftmann <none@none> |
adjusted to tightened specification of classes bot and top
|
| #
55a5de32 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
| #
f90f9f76 |
|
23-Mar-2009 |
haftmann <none@none> |
added instances for bot, top, wellorder
|
| #
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
| #
ef956639 |
|
26-Jun-2008 |
haftmann <none@none> |
established Plain theory and image
|
| #
b00cbd53 |
|
12-Mar-2008 |
haftmann <none@none> |
dropped dangerous antiquotation
|
| #
f0652a72 |
|
12-Mar-2008 |
haftmann <none@none> |
better improvement in instantiation target
|
| #
47632351 |
|
12-Mar-2008 |
haftmann <none@none> |
*** empty log message ***
|
| #
f4a615d4 |
|
07-Mar-2008 |
haftmann <none@none> |
added Option_ord.thy
|