| #
f5c4fc86 |
|
24-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
1b7e5848 |
|
16-Jan-2018 |
wenzelm <none@none> |
tuned document;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
d42838c4 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
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;
|
| #
f55b23fd |
|
23-Jul-2015 |
wenzelm <none@none> |
more symbols by default, without xsymbols mode;
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
b8e4cb1b |
|
18-Mar-2014 |
wenzelm <none@none> |
tuned signature -- rearranged modules;
|
| #
511f9921 |
|
20-May-2013 |
wenzelm <none@none> |
proper context;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
d8ea875e |
|
12-Apr-2013 |
wenzelm <none@none> |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
9626f2ce |
|
20-Nov-2011 |
wenzelm <none@none> |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
| #
335fd006 |
|
10-Sep-2011 |
wenzelm <none@none> |
misc tuning and clarification;
|
| #
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
| #
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
5d2a8866 |
|
12-May-2011 |
wenzelm <none@none> |
prefer Proof.context over old-style clasimpset;
|
| #
b97be2fb |
|
22-Nov-2010 |
hoelzl <none@none> |
Replace surj by abbreviation; remove surj_on.
|
| #
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
| #
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
| #
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
| #
8613957b |
|
27-Jul-2010 |
haftmann <none@none> |
delete structure Basic_Record; avoid `record` in names in structure Record
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
| #
7411135a |
|
22-Jul-2009 |
haftmann <none@none> |
moved complete_lattice &c. into separate theory
--HG--
rename : src/HOL/Set.thy => src/HOL/Complete_Lattice.thy
|
| #
b1258973 |
|
16-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
| #
ca494c06 |
|
15-Mar-2009 |
wenzelm <none@none> |
simplified attribute setup;
|
| #
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
| #
9d700b17 |
|
27-Jan-2008 |
wenzelm <none@none> |
rename_client_map_tac: avoid ill-defined thm reference;
|
| #
99b04075 |
|
03-Aug-2007 |
wenzelm <none@none> |
misc cleanup of ML bindings (for multihreading);
|
| #
d6c6c9ba |
|
08-Dec-2006 |
paulson <none@none> |
patched up the proofs agsin
|
| #
9f120b31 |
|
05-Dec-2006 |
wenzelm <none@none> |
removed legacy ML bindings;
|
| #
37619b7f |
|
03-Dec-2006 |
wenzelm <none@none> |
converted legacy ML script;
|
| #
82906a5c |
|
07-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
| #
7ebc34e1 |
|
22-Jul-2004 |
nipkow <none@none> |
Modified \<Sum> syntax a little.
|
| #
97364c8e |
|
15-Oct-2001 |
wenzelm <none@none> |
setsum syntax;
|
| #
64484fd5 |
|
05-Mar-2001 |
paulson <none@none> |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|