#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
6124ca59 |
|
03-Jan-2019 |
wenzelm <none@none> |
isabelle update_inner_syntax_cartouches;
|
#
8faaa443 |
|
23-May-2016 |
wenzelm <none@none> |
embedded content may be delimited via cartouches;
|
#
65f3e853 |
|
01-Jan-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
ac17d4f6 |
|
19-Oct-2015 |
wenzelm <none@none> |
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
|
#
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
886ea47b |
|
09-Apr-2015 |
wenzelm <none@none> |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
#
b88d1a76 |
|
06-Apr-2015 |
wenzelm <none@none> |
tuned;
|
#
7b5a8c0d |
|
06-Apr-2015 |
wenzelm <none@none> |
local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
|
#
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;
|
#
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
28742b1e |
|
22-Jan-2014 |
wenzelm <none@none> |
tuned signature;
|
#
e2b1c322 |
|
30-May-2013 |
wenzelm <none@none> |
tuned import;
|
#
0e2280bb |
|
27-Apr-2013 |
wenzelm <none@none> |
uniform Proof.context for hyp_subst_tac;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
bd10f13d |
|
10-Apr-2013 |
wenzelm <none@none> |
discontinued obsolete ML antiquotation @{claset};
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
e0a1c5cb |
|
11-Aug-2012 |
wenzelm <none@none> |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
90b3bab1 |
|
27-Nov-2011 |
wenzelm <none@none> |
more antiquotations;
|
#
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
7c924c4a |
|
20-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
de5f70ff |
|
27-Jun-2011 |
wenzelm <none@none> |
ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
|
#
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
#
6bf4549e |
|
14-May-2011 |
wenzelm <none@none> |
simplified BLAST_DATA;
|
#
a6a9e8cb |
|
14-May-2011 |
wenzelm <none@none> |
modernized functor names; tuned;
|
#
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;
|
#
2935cfd5 |
|
26-Apr-2011 |
wenzelm <none@none> |
simplified Blast setup;
|
#
c6e0bbb6 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
b95224b1 |
|
22-Apr-2011 |
wenzelm <none@none> |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
|
#
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
#
b4763bb2 |
|
21-Apr-2011 |
wenzelm <none@none> |
clarified simpset setup; discontinued unused old-style FOL_css;
|
#
66d530fc |
|
23-Feb-2011 |
noschinl <none@none> |
setup case_product attribute in HOL and FOL
|
#
db3d92c6 |
|
18-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
#
f95e18b9 |
|
20-Dec-2010 |
wenzelm <none@none> |
proper identifiers for consts and types;
|
#
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
#
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
#
bcf97d8c |
|
30-Jan-2010 |
berghofe <none@none> |
Adapted to changes in setup of cases method.
|
#
db994bf7 |
|
10-Jan-2010 |
berghofe <none@none> |
Adapted to changes in setup of induct method.
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
b0aa6780 |
|
28-Jul-2009 |
wenzelm <none@none> |
removed old global get_claset/map_claset; added local get_claset/put_claset;
|
#
1aee640d |
|
24-Jul-2009 |
wenzelm <none@none> |
renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
|
#
5b39ffa4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed functor InductFun to Induct;
|
#
b305563f |
|
09-Jul-2009 |
wenzelm <none@none> |
removed obsolete CVS Ids;
|
#
b1258973 |
|
16-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
#
b08c2db5 |
|
19-Nov-2008 |
wenzelm <none@none> |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
#
74823c96 |
|
28-Oct-2008 |
ballarin <none@none> |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
#
0f5001b2 |
|
15-Aug-2008 |
wenzelm <none@none> |
Args.name_source(_position) for proper position information;
|
#
d034ad82 |
|
13-Aug-2008 |
wenzelm <none@none> |
tuned document;
|
#
fe16ec1f |
|
16-Jun-2008 |
wenzelm <none@none> |
pervasive RuleInsts;
|
#
3541700d |
|
14-Jun-2008 |
wenzelm <none@none> |
removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;
|
#
5f4afb25 |
|
10-Jun-2008 |
wenzelm <none@none> |
eliminated obsolete case_split_thm -- use case_split;
|
#
1a1b9232 |
|
29-Mar-2008 |
wenzelm <none@none> |
purely functional setup of claset/simpset/clasimpset;
|
#
ae254b22 |
|
26-Mar-2008 |
wenzelm <none@none> |
pass imp_elim, swap to classical prover;
|
#
28f511f9 |
|
15-Mar-2008 |
wenzelm <none@none> |
added lemmas from simpdata.ML;
|
#
2cfeb9f2 |
|
04-Oct-2007 |
wenzelm <none@none> |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
#
7140f59e |
|
31-Jul-2007 |
wenzelm <none@none> |
moved classical tools from theory IFOL to FOL;
|
#
971cea43 |
|
31-May-2007 |
wenzelm <none@none> |
tuned header;
|
#
d06ce1ce |
|
20-Jan-2007 |
wenzelm <none@none> |
tuned ML setup;
|
#
fcd0176f |
|
26-Nov-2006 |
wenzelm <none@none> |
converted legacy ML scripts;
|
#
1f27d6b3 |
|
27-Jul-2006 |
wenzelm <none@none> |
tuned proofs;
|
#
ce464c43 |
|
28-Jan-2006 |
wenzelm <none@none> |
tuned proofs;
|
#
11bca33a |
|
06-Jan-2006 |
wenzelm <none@none> |
simplified EqSubst setup;
|
#
be73e70d |
|
06-Jan-2006 |
wenzelm <none@none> |
tuned EqSubst setup;
|
#
2cc8a738 |
|
31-Dec-2005 |
wenzelm <none@none> |
removed obsolete cla_dist_concl;
|
#
8cebd6de |
|
30-Dec-2005 |
wenzelm <none@none> |
provide cla_dist_concl;
|
#
d68c2afa |
|
23-Dec-2005 |
wenzelm <none@none> |
removed obsolete induct_atomize_old;
|
#
d01a7f2d |
|
21-Dec-2005 |
wenzelm <none@none> |
updated auxiliary facts for induct method;
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
#
a8bc5dfa |
|
08-Jul-2004 |
wenzelm <none@none> |
removed obsolete dependency;
|
#
2d476684 |
|
20-Aug-2003 |
paulson <none@none> |
new case_tac method
|
#
f20fd816 |
|
01-Jul-2003 |
paulson <none@none> |
moved some lemmas here from ZF
|
#
084e5d05 |
|
30-Aug-2002 |
paulson <none@none> |
removal of blast.overloaded
|
#
7d3d7f51 |
|
04-Dec-2001 |
wenzelm <none@none> |
removed declaration of disjI1, disjI2 (already done in IFOL);
|
#
1d975007 |
|
27-Nov-2001 |
wenzelm <none@none> |
tuned;
|
#
4868bff8 |
|
19-Nov-2001 |
wenzelm <none@none> |
induct method: localize rews for rule;
|
#
e4078174 |
|
12-Nov-2001 |
wenzelm <none@none> |
induct_atomize: include atomize_conj (for mutual induction);
|
#
b0cbf7ae |
|
12-Nov-2001 |
wenzelm <none@none> |
val local_imp_def = thm "induct_implies_def";
|
#
c91cf136 |
|
09-Nov-2001 |
wenzelm <none@none> |
theorems case_split = case_split_thm [case_names True False, cases type: o];
|
#
494d9dda |
|
30-Oct-2001 |
wenzelm <none@none> |
induct_impliesI;
|
#
9dc8a5f1 |
|
20-Oct-2001 |
wenzelm <none@none> |
calculational rules moved from FOL to IFOL;
|
#
3cb3797d |
|
14-Oct-2001 |
wenzelm <none@none> |
moved rulify to ObjectLogic;
|
#
5907fca5 |
|
04-Oct-2001 |
wenzelm <none@none> |
moved atomize stuff to theory IFOL; added induct/cases setup;
|
#
e3f5e97a |
|
11-Feb-2001 |
wenzelm <none@none> |
tuned trans rules;
|
#
abf7278a |
|
10-Nov-2000 |
wenzelm <none@none> |
added atomize_eq;
|
#
038d4a8e |
|
03-Nov-2000 |
wenzelm <none@none> |
"atomize" for classical tactics;
|
#
7d6aafc4 |
|
02-Oct-2000 |
wenzelm <none@none> |
added == transitive rule (bad idea??);
|
#
64140fbb |
|
07-Sep-2000 |
wenzelm <none@none> |
setup Rulify.setup;
|
#
4d41c00b |
|
28-Aug-2000 |
wenzelm <none@none> |
cong setup now part of Simplifier;
|
#
cb501581 |
|
04-Aug-2000 |
wenzelm <none@none> |
lemmas atomize = all_eq imp_eq;
|
#
25c11ced |
|
01-Aug-2000 |
wenzelm <none@none> |
improved comments; added all_eq, imp_eq (for blast); basic calculational rules;
|
#
58b7525b |
|
31-Mar-2000 |
wenzelm <none@none> |
added cong atts;
|
#
243ec8ac |
|
15-Mar-2000 |
wenzelm <none@none> |
splitter setup;
|
#
649c6263 |
|
25-Aug-1999 |
wenzelm <none@none> |
proper bootstrap of IFOL/FOL theories and packages;
|
#
061983f1 |
|
16-Nov-1998 |
wenzelm <none@none> |
attrib_setup;
|
#
d7a26e1a |
|
29-Apr-1998 |
wenzelm <none@none> |
tuned setup;
|
#
f39aace0 |
|
03-Apr-1998 |
wenzelm <none@none> |
replaced thy_data by thy_setup;
|
#
df94b5e6 |
|
02-Nov-1997 |
wenzelm <none@none> |
added claset thy_data;
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|