#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
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
|
#
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
|
#
ce5e3fc9 |
|
18-Feb-2014 |
kuncar <none@none> |
simplify proofs because of the stronger reflexivity prover
|
#
ef961a3d |
|
23-Jan-2014 |
nipkow <none@none> |
installed by Johannes in Extended now
|
#
6e5204b4 |
|
23-Jan-2014 |
nipkow <none@none> |
hide Fin in output of value via postprocessor; no hinding needed elsewhere
|
#
0a678c71 |
|
20-Jan-2014 |
nipkow <none@none> |
tuned names
|
#
88f16c1d |
|
06-Sep-2013 |
noschinl <none@none> |
use case_of_simps
|
#
747b2ee1 |
|
03-Jul-2013 |
nipkow <none@none> |
tuned names
|
#
01e7a4f2 |
|
14-May-2013 |
kuncar <none@none> |
stronger reflexivity prover
|
#
8086b9a8 |
|
13-May-2013 |
nipkow <none@none> |
tuned names
|
#
3d436895 |
|
08-May-2013 |
nipkow <none@none> |
standard ivl notation [l,h]
|
#
26e7c1b3 |
|
07-May-2013 |
nipkow <none@none> |
hide Fin on output
|
#
17e59550 |
|
07-May-2013 |
nipkow <none@none> |
tuned name: filter -> constrain (longer but more intuitive)
|
#
470ba361 |
|
06-May-2013 |
nipkow <none@none> |
tuned
|
#
50d4b448 |
|
06-May-2013 |
nipkow <none@none> |
improved defns and proofs
|
#
0ff76f5a |
|
05-May-2013 |
nipkow <none@none> |
simplified proofs
|
#
3cd84072 |
|
02-May-2013 |
nipkow <none@none> |
added lemma
|
#
1ddb4822 |
|
02-May-2013 |
nipkow <none@none> |
added lemma
|
#
619d5137 |
|
29-Apr-2013 |
nipkow <none@none> |
canonical names of classes
|
#
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
|
#
f06c7f68 |
|
06-Mar-2013 |
nipkow <none@none> |
major redesign: order instead of preorder, new definition of intervals as quotients
|
#
3b607ab4 |
|
24-Feb-2013 |
nipkow <none@none> |
improved orderings
|
#
7a98d079 |
|
22-Feb-2013 |
nipkow <none@none> |
more abstract intervals
|
#
e9783ae7 |
|
12-Feb-2013 |
nipkow <none@none> |
tuned top
|
#
eb80be15 |
|
25-Jan-2013 |
nipkow <none@none> |
tuned
|
#
69f2cf2f |
|
25-Sep-2012 |
nipkow <none@none> |
tuned
|
#
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
|
#
23bc83b2 |
|
19-Apr-2012 |
nipkow <none@none> |
added revised version of Abs_Int
|