| #
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;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
fb4de08a |
|
07-Nov-2017 |
nipkow <none@none> |
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
7b0aa853 |
|
19-Dec-2015 |
haftmann <none@none> |
abandoned attempt to unify sublocale and interpretation into global theories
|
| #
b2dfeb3f |
|
14-Nov-2015 |
haftmann <none@none> |
prefer "rewrites" and "defines" to note rewrite morphisms
--HG--
extra : rebase_source : db946849cc605955aa705d31965275c62fa42379
|
| #
db4d66be |
|
15-Sep-2015 |
nipkow <none@none> |
goali -> i
|
| #
c3bd9e8d |
|
19-Feb-2014 |
haftmann <none@none> |
more convenient syntax for permanent interpretation
--HG--
extra : rebase_source : 2a04f8fb415c90b0857d9553e69987e69e438c11
|
| #
d019087e |
|
19-Feb-2014 |
haftmann <none@none> |
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
--HG--
extra : rebase_source : 0e0256451de0363834f9d89306c7198ad6a4e2b2
|
| #
125c570c |
|
07-Feb-2014 |
nipkow <none@none> |
fight spurious nitpick timeouts
|
| #
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
|
| #
2eb08172 |
|
15-May-2013 |
nipkow <none@none> |
finally: acom with pointwise access and update of annotations
|
| #
8086b9a8 |
|
13-May-2013 |
nipkow <none@none> |
tuned names
|
| #
98a9e538 |
|
12-May-2013 |
nipkow <none@none> |
tuned names
|
| #
3d436895 |
|
08-May-2013 |
nipkow <none@none> |
standard ivl notation [l,h]
|
| #
808362ce |
|
07-May-2013 |
nipkow <none@none> |
tuned
|
| #
17e59550 |
|
07-May-2013 |
nipkow <none@none> |
tuned name: filter -> constrain (longer but more intuitive)
|
| #
619d5137 |
|
29-Apr-2013 |
nipkow <none@none> |
canonical names of classes
|
| #
9854b9a3 |
|
26-Apr-2013 |
nipkow <none@none> |
simplified def
|
| #
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
|
| #
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
|
| #
c1bdfac1 |
|
10-Mar-2013 |
nipkow <none@none> |
termination proof for narrowing: fewer assumptions
|
| #
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
|
| #
7a98d079 |
|
22-Feb-2013 |
nipkow <none@none> |
more abstract intervals
|
| #
e9783ae7 |
|
12-Feb-2013 |
nipkow <none@none> |
tuned top
|
| #
823eaec9 |
|
19-Jan-2013 |
nipkow <none@none> |
simplified proofs
|
| #
eb80be15 |
|
25-Jan-2013 |
nipkow <none@none> |
tuned
|
| #
dd55254d |
|
17-Oct-2012 |
wenzelm <none@none> |
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
|
| #
69f2cf2f |
|
25-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
f730c12e |
|
25-Sep-2012 |
nipkow <none@none> |
added counterexamples
|
| #
9a14259d |
|
24-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
979091bc |
|
24-Sep-2012 |
nipkow <none@none> |
generalized types
|
| #
51dbf8b4 |
|
23-Sep-2012 |
nipkow <none@none> |
tuned termination proof
|
| #
713ac2bf |
|
21-Sep-2012 |
nipkow <none@none> |
more termination proofs
|
| #
ffb47d43 |
|
16-Sep-2012 |
nipkow <none@none> |
tuned
|
| #
3f59dca8 |
|
16-Sep-2012 |
nipkow <none@none> |
converted wt into a set, tuned names
|
| #
5e83833a |
|
06-Sep-2012 |
nipkow <none@none> |
adjusted examples
|
| #
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
|
| #
23bc83b2 |
|
19-Apr-2012 |
nipkow <none@none> |
added revised version of Abs_Int
|