History log of /seL4-l4v-master/isabelle/src/Sequents/LK0.thy
Revision Date Author Comments
# f8a2f58b 15-Oct-2019 wenzelm <none@none>

set_preproc for object-logics with type classes;


# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 0bd0d17f 10-Oct-2015 wenzelm <none@none>

more symbols;


# c333f2c0 10-Oct-2015 wenzelm <none@none>

more symbols;


# 607ae3e3 09-Oct-2015 wenzelm <none@none>

discontinued specific HTML syntax;


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

isabelle update_cartouches;


# 7f7de75b 18-Jul-2015 wenzelm <none@none>

prefer tactics with explicit context;


# 8083303a 23-Mar-2015 wenzelm <none@none>

support 'for' fixes in rule_tac etc.;


# 2d6c364b 20-Mar-2015 wenzelm <none@none>

tuned signature;


# 4e1305ff 19-Mar-2015 wenzelm <none@none>

more position information;


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

modernized header uniformly as section;


# 0551f7de 01-Nov-2014 wenzelm <none@none>

eliminated spurious semicolons;


# 82c645a3 10-Feb-2014 wenzelm <none@none>

prefer vacuous definitional type classes over axiomatic ones;


# de9860e0 01-Feb-2014 wenzelm <none@none>

method_setup "lem";


# 39978f9c 01-Feb-2014 wenzelm <none@none>

misc tuning and modernization;


# ffcd6989 25-May-2013 wenzelm <none@none>

syntax translations always depend on context;


# 25a73f94 28-Feb-2013 wenzelm <none@none>

eliminated legacy 'axioms';


# 29168e90 20-Nov-2011 wenzelm <none@none>

eliminated obsolete "standard";


# 10eb7fb0 15-May-2011 wenzelm <none@none>

simplified/unified method_setup/attribute_setup;


# 6b0b29ec 13-Mar-2011 wenzelm <none@none>

tuned headers;


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

more antiquotations;


# 0c99426e 17-Aug-2010 haftmann <none@none>

deglobalization


# b6ea9aae 27-Apr-2010 wenzelm <none@none>

renamed command 'defaultsort' to 'default_sort';


# baea5702 01-Mar-2010 haftmann <none@none>

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)


# 942a6e5f 24-Feb-2010 wenzelm <none@none>

modernized syntax declarations, and make them actually work with authentic syntax;


# aebe6a56 11-Feb-2010 wenzelm <none@none>

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};


# b1258973 16-Mar-2009 wenzelm <none@none>

simplified method setup;


# 77d6b267 13-Mar-2009 wenzelm <none@none>

unified type Proof.method and pervasive METHOD combinators;


# fe16ec1f 16-Jun-2008 wenzelm <none@none>

pervasive RuleInsts;


# ea407404 14-Jun-2008 wenzelm <none@none>

proper context for tactics derived from res_inst_tac;


# a9475b27 11-Jun-2008 wenzelm <none@none>

more antiquotations;


# 1f37caae 09-May-2007 wenzelm <none@none>

eliminated unnamed infixes;


# f7800759 29-Nov-2006 wenzelm <none@none>

simplified method setup;


# b538f435 26-Nov-2006 wenzelm <none@none>

updated (binder) syntax/notation;


# 852bb740 20-Nov-2006 wenzelm <none@none>

removed legacy ML setup;


# 4b291da4 20-Nov-2006 wenzelm <none@none>

converted legacy ML scripts;


# 8a247b6e 18-Sep-2005 wenzelm <none@none>

converted to Isar theory format;


# 8b6756fc 22-May-2005 wenzelm <none@none>

Simplifier already setup in Pure;


# 4ca8e7a3 31-May-2004 wenzelm <none@none>

removed obsolete sort 'logic';


# 1d403847 21-May-2004 wenzelm <none@none>

proper use of 'syntax';


# cd257618 14-Apr-2004 kleing <none@none>

use more symbols in HTML output


# 39d45027 07-Jan-2002 wenzelm <none@none>

syntax "_not_equal";


# 8f38a7d6 08-Nov-2001 wenzelm <none@none>

got rid of obsolete input filtering;


# cee47ab9 03-Aug-1999 paulson <none@none>

Sara Kalvala: moving the <<...>> notation from LK to Sequents


# 33b7a216 28-Jul-1999 paulson <none@none>

adding missing declarations for the <<...>> notation


# a8e6f239 27-Jul-1999 paulson <none@none>

renamed theory LK to LK0