#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
29313743 |
|
12-Jan-2016 |
wenzelm <none@none> |
eliminated old defs;
|
#
a279bbf2 |
|
16-Dec-2015 |
wenzelm <none@none> |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
#
e11de3a7 |
|
26-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
b0d49015 |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols; eliminated alternative syntax;
|
#
69b24741 |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols;
|
#
403911ef |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
54b0f060 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
f18c332a |
|
10-Feb-2014 |
wenzelm <none@none> |
prefer vacuous definitional type classes over axiomatic ones;
|
#
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
|
#
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
#
53ded129 |
|
20-Mar-2011 |
wenzelm <none@none> |
modernized specifications;
|
#
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
#
5f258a36 |
|
26-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix impliciation now named HOL.implies
|
#
bbda5041 |
|
19-Aug-2010 |
haftmann <none@none> |
use antiquotations for remaining unqualified constants in HOL
|
#
428da570 |
|
24-Feb-2010 |
wenzelm <none@none> |
observe standard convention for syntax consts;
|
#
164ee5c8 |
|
23-Feb-2010 |
haftmann <none@none> |
dropped axclass, going back to purely syntactic type classes
|
#
bd7d809a |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized syntax/translations; tuned headers;
|
#
d62b04dd |
|
06-Jul-2009 |
wenzelm <none@none> |
structure Thm: less pervasive names;
|
#
000f32c5 |
|
05-Jun-2009 |
haftmann <none@none> |
Set.insert with authentic syntax
|
#
ca494c06 |
|
15-Mar-2009 |
wenzelm <none@none> |
simplified attribute setup;
|
#
13c78537 |
|
07-Aug-2007 |
wenzelm <none@none> |
tuned ML setup;
|
#
4a856837 |
|
01-Dec-2006 |
wenzelm <none@none> |
TLA: converted legacy ML scripts;
|
#
ee1c412f |
|
13-Oct-2006 |
berghofe <none@none> |
Adapted to changes in FixedPoint theory.
|
#
f55bd273 |
|
07-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
ace2eaf8 |
|
03-Aug-2000 |
wenzelm <none@none> |
tuned version by Stephan Merz (unbatchified etc.);
|
#
888d07b6 |
|
16-Aug-1999 |
wenzelm <none@none> |
'a list: Nil, Cons;
|
#
e2a0a88b |
|
10-Mar-1999 |
wenzelm <none@none> |
HTML output;
|
#
0c0fa6ed |
|
08-Feb-1999 |
wenzelm <none@none> |
updated (Stephan Merz);
|
#
9b6e7a832 |
|
07-Oct-1997 |
wenzelm <none@none> |
symbols syntax;
|
#
8b3b3609 |
|
08-Oct-1997 |
wenzelm <none@none> |
A formalization of TLA in HOL -- by Stephan Merz;
|