History log of /seL4-l4v-master/isabelle/src/CTT/ex/Elimination.thy
Revision Date Author Comments
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 97b498a1 03-Feb-2017 wenzelm <none@none>

misc tuning;


# 296730b5 15-Jul-2016 wenzelm <none@none>

misc tuning and modernization;
proper document setup;


# 03b18167 10-Oct-2015 wenzelm <none@none>

tuned syntax -- more symbols;


# 56730d74 06-Oct-2015 wenzelm <none@none>

fewer aliases for toplevel theorem statements;


# 8ecffcf0 23-Jul-2015 wenzelm <none@none>

isabelle update_cartouches;


# b8d56fe6 10-Feb-2015 wenzelm <none@none>

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;


# bf6c9bb9 11-Nov-2014 wenzelm <none@none>

more symbols;


# 9913ba16 11-Nov-2014 wenzelm <none@none>

simplifie sessions;


# b4f93635 11-Nov-2014 wenzelm <none@none>

more Isar proof methods;


# 4eae0352 10-Nov-2014 wenzelm <none@none>

proper context for assume_tac (atac remains as fall-back without context);


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

modernized header uniformly as section;


# 80a964bc 12-Jan-2011 wenzelm <none@none>

eliminated global prems;


# 27ff3609 06-Sep-2010 wenzelm <none@none>

more antiquotations;


# 52bca335 23-Apr-2010 wenzelm <none@none>

mark schematic statements explicitly;


# 458a4961 13-Mar-2010 wenzelm <none@none>

removed old CVS Ids;
tuned headers;


# f03cdfbf 02-Jun-2006 wenzelm <none@none>

removed obsolete ML files;