History log of /seL4-l4v-master/isabelle/src/HOL/ex/Adhoc_Overloading_Examples.thy
Revision Date Author Comments
# e5238d11 28-Jan-2019 nipkow <none@none>

more canonical and less specialized syntax


# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 17bc899d 18-Aug-2017 wenzelm <none@none>

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;


# 0fcdba11 06-Aug-2017 haftmann <none@none>

do not fall back on nbe if plain evaluation fails

--HG--
extra : rebase_source : 39c0db3b5b4b140dfa4b9ec4b73134a3126ac472


# ca5f3a9e 20-Jul-2016 wenzelm <none@none>

provide Pure.simp/simp_all, which only know about meta-equality;


# 36e39dcf 26-Dec-2015 wenzelm <none@none>

isabelle update_cartouches -c -t;


# ee8e8234 06-Oct-2015 wenzelm <none@none>

isabelle update_cartouches;


# 5012105f 13-Sep-2015 wenzelm <none@none>

tuned proofs -- less legacy;


# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;


# 5fc26177 11-Sep-2014 blanchet <none@none>

updated news


# d2ddb3a1 09-Sep-2014 blanchet <none@none>

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries


# e46c07fd 04-Jul-2014 haftmann <none@none>

reduced name variants for assoc and commute on plus and mult


# 4177ebe5 04-Jul-2014 wenzelm <none@none>

revived unchecked theory (see cebaf814ca6e);


# 313f051f 11-Sep-2013 wenzelm <none@none>

tuned whitespace;


# c651c015 02-Aug-2013 Christian Sternagel <none@none>

added examples of adhoc overloading