History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
Revision Date Author Comments
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;
# fcc9e542 23-Feb-2018 wenzelm <none@none>

added HOLogic.mk_obj_eq convenience and eliminated some clones;
# 58bef678 24-Oct-2016 traytel <none@none>

additional user-specified simp (naturality) rules used in friend_of_corec
# 908e2607 12-Sep-2016 blanchet <none@none>

moved ML function
# c478d6ef 04-Apr-2016 wenzelm <none@none>

tuned headers;
# a65d036e 29-Mar-2016 blanchet <none@none>

try tactics in right order w.r.t. schematics
# dffe416d 27-Mar-2016 blanchet <none@none>

tuning
# 16a073ce 27-Mar-2016 blanchet <none@none>

strengthened tactic
# d80c5394 21-Mar-2016 blanchet <none@none>

moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle