| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
5589896c |
|
12-Jan-2018 |
wenzelm <none@none> |
isabelle update_cartouches -c;
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
5eeb10d5 |
|
19-Aug-2015 |
paulson <lp15@cam.ac.uk> |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
8854b93e |
|
15-Jan-2014 |
nipkow <none@none> |
tuned
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
| #
747b2ee1 |
|
03-Jul-2013 |
nipkow <none@none> |
tuned names
|
| #
83572917 |
|
17-May-2013 |
nipkow <none@none> |
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
|
| #
8086b9a8 |
|
13-May-2013 |
nipkow <none@none> |
tuned names
|
| #
260ecc8f |
|
09-May-2013 |
nipkow <none@none> |
tuned
|
| #
619d5137 |
|
29-Apr-2013 |
nipkow <none@none> |
canonical names of classes
|
| #
d006ad06 |
|
26-Apr-2013 |
nipkow <none@none> |
more standard argument order
|
| #
3b4ffced |
|
26-Apr-2013 |
nipkow <none@none> |
simplified def
|
| #
2ee1ba3a |
|
26-Apr-2013 |
nipkow <none@none> |
more standard order of arguments
|
| #
802adb4a |
|
20-Apr-2013 |
nipkow <none@none> |
proved termination for fun-based AI
|
| #
83a53146 |
|
17-Apr-2013 |
nipkow <none@none> |
tuned
|
| #
772233d8 |
|
17-Apr-2013 |
nipkow <none@none> |
complete revision: finally got rid of annoying L-predicate
|
| #
1809d7e0 |
|
10-Mar-2013 |
nipkow <none@none> |
more factorisation of Step & Co
|
| #
a7bab1ad |
|
10-Mar-2013 |
nipkow <none@none> |
factored out Step
|
| #
458d320c |
|
08-Mar-2013 |
nipkow <none@none> |
simplified basic termination proof
|
| #
f06c7f68 |
|
06-Mar-2013 |
nipkow <none@none> |
major redesign: order instead of preorder, new definition of intervals as quotients
|
| #
e9783ae7 |
|
12-Feb-2013 |
nipkow <none@none> |
tuned top
|
| #
823eaec9 |
|
19-Jan-2013 |
nipkow <none@none> |
simplified proofs
|
| #
caa53062 |
|
15-Jan-2013 |
nipkow <none@none> |
tuned
|
| #
51dbf8b4 |
|
23-Sep-2012 |
nipkow <none@none> |
tuned termination proof
|
| #
4964a819 |
|
21-Sep-2012 |
nipkow <none@none> |
tuned names
|
| #
43af1f10 |
|
19-Sep-2012 |
nipkow <none@none> |
removed lpfp and proved least pfp thm
|
| #
95bfe5d8 |
|
17-Sep-2012 |
nipkow <none@none> |
beautified names
|
| #
47ed2dfd |
|
17-Sep-2012 |
nipkow <none@none> |
proved all upper bounds
|
| #
56a073d2 |
|
17-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
3f59dca8 |
|
16-Sep-2012 |
nipkow <none@none> |
converted wt into a set, tuned names
|
| #
b7bc8082 |
|
14-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
8d45020a |
|
13-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
629c206f |
|
03-Sep-2012 |
nipkow <none@none> |
added annotations after condition in if and while
|
| #
928c96fc |
|
10-Aug-2012 |
nipkow <none@none> |
Improved complete lattice formalisation - no more index set.
--HG--
rename : src/HOL/IMP/Collecting.thy => src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
rename : src/HOL/IMP/Complete_Lattice_ix.thy => src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy
|
| #
fc1f85e4 |
|
27-Apr-2012 |
nipkow <none@none> |
renamed Semi to Seq
|
| #
23bc83b2 |
|
19-Apr-2012 |
nipkow <none@none> |
added revised version of Abs_Int
|
| #
1e81e115 |
|
29-Jan-2012 |
nipkow <none@none> |
removed accidental dependance of abstract interpreter on gamma
|
| #
6719c874 |
|
27-Jan-2012 |
nipkow <none@none> |
removed duplicate definitions that made locale inconsistent
|
| #
bb907fd9 |
|
19-Jan-2012 |
nipkow <none@none> |
added termination of narrowing
|
| #
61387c28 |
|
18-Jan-2012 |
nipkow <none@none> |
introduced commands over a set of vars
|
| #
f556ddf1 |
|
07-Jan-2012 |
nipkow <none@none> |
tuned
|
| #
52c5670e |
|
02-Jan-2012 |
nipkow <none@none> |
tuned
|
| #
4b3d8b85 |
|
02-Jan-2012 |
nipkow <none@none> |
tuned proofs
|
| #
ba69bca5 |
|
01-Jan-2012 |
nipkow <none@none> |
tuned var names
|
| #
23ae8a74 |
|
01-Jan-2012 |
nipkow <none@none> |
tuned argument order
|
| #
b0324e93 |
|
31-Dec-2011 |
nipkow <none@none> |
tuned types
|
| #
2be6a206 |
|
29-Dec-2011 |
nipkow <none@none> |
tuned
|
| #
d16c96ab |
|
15-Dec-2011 |
nipkow <none@none> |
improved indexed complete lattice
|
| #
be133f23 |
|
27-Nov-2011 |
nipkow <none@none> |
simplified Collecting1 and renamed: step -> step', step_cs -> step
|
| #
3b967237 |
|
24-Nov-2011 |
nipkow <none@none> |
Abstract interpretation is now based uniformly on annotated programs,
including a collecting and a small step semantics
|
| #
b70c32f7 |
|
19-Oct-2011 |
nipkow <none@none> |
renamed B to Bc
|
| #
fa1d1d8e |
|
12-Oct-2011 |
nipkow <none@none> |
separated monotonicity reasoning and defined narrowing with while_option
|
| #
57fa7769 |
|
28-Sep-2011 |
nipkow <none@none> |
Added Hoare-like Abstract Interpretation
--HG--
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy => src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
rename : src/HOL/IMP/Abs_Int_Den/Abs_State.thy => src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy
|