| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
fe9ee25d |
|
22-Jan-2018 |
Lars Hupel <lars.hupel@mytum.de> |
drop redundant fundef_cong rule
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
8863117a |
|
17-Dec-2016 |
haftmann <none@none> |
restructured matter on polynomials and normalized fractions
--HG--
extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625
|
| #
1667fe95 |
|
10-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
2dc6f8f0 |
|
11-Jul-2016 |
wenzelm <none@none> |
tuned;
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
df44ab4c |
|
27-Aug-2015 |
haftmann <none@none> |
standardized some occurences of ancient "split" alias
--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
a7d3b0ad |
|
07-Jul-2015 |
blanchet <none@none> |
have the installed termination prover take a 'quiet' flag
|
| #
8a1b73d1 |
|
08-Apr-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
efcf16e5 |
|
14-Dec-2014 |
blanchet <none@none> |
renamed theory file
--HG--
rename : src/HOL/Basic_BNF_Least_Fixpoints.thy => src/HOL/Basic_BNF_LFPs.thy
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
| #
6d42cd2f |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
tuned whitespace;
|
| #
9b903e0e |
|
18-Sep-2014 |
blanchet <none@none> |
moved old 'size' generator together with 'old_datatype'
--HG--
rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML
|
| #
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
| #
b1da7acd |
|
18-Aug-2014 |
wenzelm <none@none> |
simplified type Proof.method;
|
| #
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems;
modernized module name and setup;
|
| #
b3e5b66d |
|
04-May-2014 |
blanchet <none@none> |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
| #
0811cf40 |
|
23-Apr-2014 |
blanchet <none@none> |
move size hooks together, with new one preceding old one and sharing same theory data
|
| #
03184bca |
|
22-Mar-2014 |
haftmann <none@none> |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
| #
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
| #
447c00c8 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'Option.map' and 'Option.map_option'
|
| #
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|