#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
#
56a6bda0 |
|
10-Oct-2015 |
wenzelm <none@none> |
tuned syntax -- more symbols;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
26c71f46 |
|
19-Mar-2015 |
wenzelm <none@none> |
slightly more formal historic examples;
|
#
eeb00f20 |
|
11-Feb-2015 |
wenzelm <none@none> |
proper context; tuned whitespace;
|
#
76fae1a7 |
|
21-Aug-2014 |
haftmann <none@none> |
integrated appendix theory into main theory; tuned ML --HG-- extra : rebase_source : a066b231916d8839dd4199f5a608ee49e36e9fd9
|
#
5be1d78d |
|
11-Nov-2013 |
wenzelm <none@none> |
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
527a4060 |
|
17-Sep-2011 |
haftmann <none@none> |
dropped unused argument – avoids problem with SML/NJ
|
#
f65bae10 |
|
02-Dec-2010 |
wenzelm <none@none> |
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
|
#
ce929d7f |
|
03-Nov-2010 |
wenzelm <none@none> |
eliminated dead code;
|
#
caf0b475 |
|
03-Nov-2010 |
wenzelm <none@none> |
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;
|
#
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
#
2b1723df |
|
28-Feb-2010 |
wenzelm <none@none> |
more antiquotations; eliminated legacy ML bindings;
|
#
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
#
5404b7b7 |
|
13-Feb-2010 |
wenzelm <none@none> |
modernized structures;
|
#
7882ab22 |
|
11-Feb-2010 |
wenzelm <none@none> |
numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
|
#
535cdf2f |
|
07-Feb-2010 |
wenzelm <none@none> |
prefer explicit @{lemma} over adhoc forward reasoning;
|
#
a2aef54e |
|
16-Oct-2009 |
wenzelm <none@none> |
explicitly qualify Drule.standard;
|
#
92e775bc |
|
23-Jul-2009 |
wenzelm <none@none> |
more @{theory} antiquotations;
|
#
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;
|
#
2251533a |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
c5767bd5 |
|
16-Jun-2008 |
wenzelm <none@none> |
converted ML proofs;
|
#
6284a6de |
|
11-Jun-2008 |
wenzelm <none@none> |
OldGoals.inst;
|
#
58770cf0 |
|
01-Mar-2008 |
wenzelm <none@none> |
tuned ML code, more antiquotations;
|
#
04640bf0 |
|
11-Feb-2008 |
wenzelm <none@none> |
removed unnecessary theory qualifiers;
|
#
4754b723 |
|
11-Feb-2008 |
krauss <none@none> |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
|
#
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications; removed legacy ML bindings;
|
#
2a4bde03 |
|
18-Sep-2007 |
wenzelm <none@none> |
simplified type int (eliminated IntInf.int, integer);
|
#
2a6a445f |
|
30-May-2007 |
wenzelm <none@none> |
moved Integ files to canonical place;
|