#
450e4fbf |
|
05-Dec-2019 |
haftmann <none@none> |
more direct accessors for simpset
|
#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
4bad625f |
|
03-Jun-2019 |
wenzelm <none@none> |
clarified signature;
|
#
0ed93039 |
|
04-Jan-2019 |
wenzelm <none@none> |
support for isabelle update -u control_cartouches;
|
#
26e81017 |
|
27-Nov-2018 |
wenzelm <none@none> |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
|
#
2b1ecb7f |
|
06-Jun-2018 |
nipkow <none@none> |
reorient -> split; documented split
|
#
b402d35b |
|
26-Apr-2018 |
nipkow <none@none> |
new simp modifier: reorient
|
#
9dda44c3 |
|
01-Feb-2018 |
wenzelm <none@none> |
clarified signature: prefer proper order operation;
|
#
8274f3e0 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
004a5084 |
|
06-Dec-2017 |
wenzelm <none@none> |
more embedded cartouche arguments; more uniform LaTeX output for control symbols;
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
ca5f3a9e |
|
20-Jul-2016 |
wenzelm <none@none> |
provide Pure.simp/simp_all, which only know about meta-equality;
|
#
9619db56 |
|
02-Jun-2016 |
wenzelm <none@none> |
avoid warnings on duplicate rules in the given list;
|
#
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
#
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;
|
#
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
|
#
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
#
58b37d08 |
|
09-Sep-2015 |
wenzelm <none@none> |
clarified declaration flags, like 'declaration' command;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
e2360983 |
|
02-Sep-2015 |
wenzelm <none@none> |
eliminated pointless cterms;
|
#
94e11df0 |
|
03-Apr-2015 |
wenzelm <none@none> |
more uniform "verbose" option to print name space;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
e3946d66 |
|
01-Mar-2015 |
wenzelm <none@none> |
added Proof_Context.cterm_of/ctyp_of convenience;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
#
78821146 |
|
27-Aug-2014 |
wenzelm <none@none> |
more explicit Method.modifier with reported position;
|
#
e1988415 |
|
19-Aug-2014 |
wenzelm <none@none> |
added PARALLEL_ALLGOALS convenience;
|
#
dd622849 |
|
09-Apr-2014 |
wenzelm <none@none> |
added simproc markup, which also indicates legacy simprocs outside the name space;
|
#
08fb3b84 |
|
18-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
42ab7e1e |
|
12-Mar-2014 |
wenzelm <none@none> |
tuned signature -- clarified module name; --HG-- rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML
|
#
cc39ff13 |
|
12-Jan-2014 |
wenzelm <none@none> |
proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;
|
#
65c6de1e |
|
12-Dec-2013 |
wenzelm <none@none> |
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
|
#
f19a8d08 |
|
12-Dec-2013 |
wenzelm <none@none> |
generic trace operations for main steps of Simplifier;
|
#
acb34a00 |
|
12-Dec-2013 |
wenzelm <none@none> |
tuned signature;
|
#
5be1d78d |
|
11-Nov-2013 |
wenzelm <none@none> |
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
|
#
a66c9494 |
|
23-Aug-2013 |
wenzelm <none@none> |
added Theory.setup convenience;
|
#
906d4fba |
|
26-Jun-2013 |
wenzelm <none@none> |
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
2a99e898 |
|
10-Apr-2013 |
wenzelm <none@none> |
obsolete -- tools should refer to proper Proof.context;
|
#
b0bd12e2 |
|
30-Mar-2013 |
wenzelm <none@none> |
more formal cong_name;
|
#
0493e8f8 |
|
30-Mar-2013 |
wenzelm <none@none> |
more item markup; tuned signature;
|
#
00bf81f2 |
|
29-Mar-2013 |
wenzelm <none@none> |
Pretty.item markup for improved readability of lists of items;
|
#
09e81af1 |
|
17-Nov-2012 |
wenzelm <none@none> |
tuned signature;
|
#
e0a1c5cb |
|
11-Aug-2012 |
wenzelm <none@none> |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
#
526eba8a |
|
14-Apr-2012 |
wenzelm <none@none> |
outermost SELECT_GOAL potentially improves performance;
|
#
14c5ca62 |
|
31-Mar-2012 |
wenzelm <none@none> |
tuned signature;
|
#
551b966c |
|
18-Mar-2012 |
wenzelm <none@none> |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
|
#
7d260991 |
|
17-Mar-2012 |
wenzelm <none@none> |
proper naming of simprocs according to actual target context; afford pervasive declaration which makes results available with qualified name from outside;
|
#
124bff6d |
|
03-Mar-2012 |
wenzelm <none@none> |
tuned;
|
#
ce167a73 |
|
14-Feb-2012 |
wenzelm <none@none> |
tuned signature;
|
#
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
9fa04411 |
|
06-Nov-2011 |
wenzelm <none@none> |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
|
#
98b3e422 |
|
03-Nov-2011 |
wenzelm <none@none> |
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
|
#
01244fea |
|
28-Oct-2011 |
wenzelm <none@none> |
uniform Local_Theory.declaration with explicit params;
|
#
a309722d |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned signature -- refined terminology;
|
#
4911f028 |
|
08-Aug-2011 |
wenzelm <none@none> |
misc tuning -- eliminated old-fashioned rep_thm;
|
#
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
#
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
#
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;
|
#
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;
|
#
f93e75ad |
|
23-Apr-2011 |
wenzelm <none@none> |
added Name_Space.check/get convenience;
|
#
8585b428 |
|
23-Apr-2011 |
wenzelm <none@none> |
clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;
|
#
00fc42cd |
|
23-Apr-2011 |
wenzelm <none@none> |
proper binding/report of defined simprocs; tuned signature;
|
#
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
|
#
46b14634 |
|
16-Apr-2011 |
wenzelm <none@none> |
PARALLEL_GOALS for method "simp_all";
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
ddbb3956 |
|
22-Dec-2010 |
haftmann <none@none> |
tuned comment
|
#
a4e367ec |
|
17-Dec-2010 |
wenzelm <none@none> |
more explicit references to structure Raw_Simplifier;
|
#
3272990d |
|
17-Dec-2010 |
wenzelm <none@none> |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning; --HG-- rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML
|
#
7fc0bf78 |
|
17-Dec-2010 |
wenzelm <none@none> |
clarified exports of structure Simplifier;
|
#
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;
|
#
df528aad |
|
15-Jun-2010 |
haftmann <none@none> |
tuned whitespace
|
#
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
#
60d6d298 |
|
03-May-2010 |
wenzelm <none@none> |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
#
30b49473 |
|
30-Apr-2010 |
wenzelm <none@none> |
export Simplifier.with_context;
|
#
b00558e6 |
|
30-Apr-2010 |
wenzelm <none@none> |
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
|
#
b96c5111 |
|
29-Apr-2010 |
wenzelm <none@none> |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
#
906be7a0 |
|
06-Mar-2010 |
wenzelm <none@none> |
eliminated Args.bang_facts (legacy feature);
|
#
aa047a26 |
|
19-Feb-2010 |
wenzelm <none@none> |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
#
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
#
0c9f4a61 |
|
10-Nov-2009 |
wenzelm <none@none> |
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
|
#
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data; tuned;
|
#
296c7062 |
|
05-Nov-2009 |
wenzelm <none@none> |
adapted LocalTheory.declaration;
|
#
c90943cf |
|
25-Oct-2009 |
wenzelm <none@none> |
LocalTheory.naming_of;
|
#
a00d61a9 |
|
25-Oct-2009 |
wenzelm <none@none> |
make SML/NJ happy;
|
#
aa0f9eb7 |
|
24-Oct-2009 |
wenzelm <none@none> |
maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
|
#
713fc456 |
|
24-Oct-2009 |
wenzelm <none@none> |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
#
4b3225d2 |
|
24-Oct-2009 |
wenzelm <none@none> |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
#
348d0907 |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated dead code;
|
#
b9d789f1 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
9bf7f277 |
|
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;
|
#
886198b6 |
|
20-Jul-2009 |
wenzelm <none@none> |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
#
d932372e |
|
29-May-2009 |
wenzelm <none@none> |
modernized method setup; tuned;
|
#
1716138f |
|
20-Mar-2009 |
wenzelm <none@none> |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
#
ca494c06 |
|
15-Mar-2009 |
wenzelm <none@none> |
simplified attribute setup;
|
#
da802918 |
|
13-Mar-2009 |
wenzelm <none@none> |
eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
|
#
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
#
3c4dea06 |
|
12-Mar-2009 |
wenzelm <none@none> |
renamed NameSpace.bind to NameSpace.define;
|
#
4768c4a8 |
|
07-Mar-2009 |
wenzelm <none@none> |
added dest_ss; proper context fo pretty_ss; tuned;
|
#
448a1992 |
|
07-Mar-2009 |
wenzelm <none@none> |
renamed rep_ss to MetaSimplifier.internal_ss;
|
#
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
#
4c569229 |
|
05-Dec-2008 |
haftmann <none@none> |
dropped NameSpace.declare_base
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
2c26594b |
|
20-Nov-2008 |
haftmann <none@none> |
dropped legacy naming code
|
#
7d0c6e82 |
|
14-Nov-2008 |
haftmann <none@none> |
namify and name_decl combinators
|
#
a66951b0 |
|
13-Nov-2008 |
haftmann <none@none> |
consider prefixes for name bindings of simprocs (a first approximation)
|
#
058e1ea3 |
|
02-Sep-2008 |
wenzelm <none@none> |
name/var morphism operates on Name.binding;
|
#
56ac4f51 |
|
24-Jun-2008 |
wenzelm <none@none> |
ML_Antiquote.value;
|
#
3b0a7b23 |
|
29-May-2008 |
wenzelm <none@none> |
proper context for attribute simplified;
|
#
d4aa0c76 |
|
15-Apr-2008 |
wenzelm <none@none> |
Thm.forall_elim_var(s);
|
#
e448476e |
|
29-Mar-2008 |
wenzelm <none@none> |
purely functional setup of claset/simpset/clasimpset; tuned signature;
|
#
55096917 |
|
28-Mar-2008 |
wenzelm <none@none> |
Context.>> : operate on Context.generic;
|
#
ebe088c1 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated delayed theory setup
|
#
be076d56 |
|
27-Mar-2008 |
wenzelm <none@none> |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
#
b1ded813 |
|
01-Sep-2007 |
wenzelm <none@none> |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
|
#
a710011c |
|
01-Aug-2007 |
wenzelm <none@none> |
turned simp_depth_limit into configuration option;
|
#
0da5ad5d |
|
28-Jul-2007 |
wenzelm <none@none> |
added attribute "simproc"; marked some CRITICAL sections; tuned;
|
#
5110e11c |
|
08-Jul-2007 |
wenzelm <none@none> |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
#
0a83a53c |
|
05-Jul-2007 |
wenzelm <none@none> |
tuned;
|
#
3c5fe34d |
|
03-Jul-2007 |
wenzelm <none@none> |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
#
99be5308 |
|
24-May-2007 |
haftmann <none@none> |
tuned Pure/General/name_space.ML
|
#
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
#
8fa68945 |
|
23-Apr-2007 |
wenzelm <none@none> |
def_simproc(_i): proper ProofContext.read/cert_terms;
|
#
b585d2bb |
|
16-Apr-2007 |
haftmann <none@none> |
canonical merge operations
|
#
10cbbe6c |
|
15-Apr-2007 |
wenzelm <none@none> |
removed obsolete TypeInfer.logicT -- use dummyT;
|
#
8a143779 |
|
28-Feb-2007 |
wenzelm <none@none> |
exported get_ss, map_ss;
|
#
c4c6862e |
|
04-Feb-2007 |
wenzelm <none@none> |
def_simproc(_i): tuned interface; tuned simprocs environment;
|
#
ed580f56 |
|
29-Jan-2007 |
wenzelm <none@none> |
added get_simproc, @{simproc};
|
#
96787e55 |
|
28-Jan-2007 |
wenzelm <none@none> |
added def_simproc(_i) -- define named simprocs; tuned;
|
#
655e75df |
|
20-Jan-2007 |
wenzelm <none@none> |
added @{simpset};
|
#
11a4159e |
|
19-Jan-2007 |
wenzelm <none@none> |
moved ML context stuff to from Context to ML_Context;
|
#
7b9d7f5f |
|
07-Dec-2006 |
wenzelm <none@none> |
reorganized structure Tactic vs. MetaSimplifier;
|
#
9989d06d |
|
06-Dec-2006 |
wenzelm <none@none> |
reorganized structure Goal vs. Tactic;
|
#
d4a85c74 |
|
09-Nov-2006 |
haftmann <none@none> |
introduces canonical AList functions for loop_tacs
|
#
f13d91fd |
|
06-Oct-2006 |
wenzelm <none@none> |
tuned;
|
#
f050d7b4 |
|
09-Feb-2006 |
wenzelm <none@none> |
Args/Attrib syntax: Context.generic;
|
#
acdc5889 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute;
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
ab6437ef |
|
14-Jan-2006 |
wenzelm <none@none> |
generic attributes;
|
#
ba3e65a4 |
|
10-Jan-2006 |
wenzelm <none@none> |
Attrib.rule;
|
#
ec821b16 |
|
28-Oct-2005 |
wenzelm <none@none> |
export cong_modifiers, simp_modifiers';
|
#
e1d3e963 |
|
21-Oct-2005 |
wenzelm <none@none> |
added simplification tactics and rules (from meta_simplifier.ML);
|
#
d8070a9b |
|
18-Oct-2005 |
wenzelm <none@none> |
renamed set_context to context; data extend: reset context;
|
#
9ad58493 |
|
17-Oct-2005 |
wenzelm <none@none> |
removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;
|
#
db7c5716 |
|
29-Sep-2005 |
wenzelm <none@none> |
export debug_bounds;
|
#
3abd6386 |
|
02-Aug-2005 |
wenzelm <none@none> |
export clear_ss;
|
#
dfa833a1 |
|
01-Aug-2005 |
wenzelm <none@none> |
export MataSimplifier.inherit_bounds;
|
#
c84c5709 |
|
13-Jul-2005 |
wenzelm <none@none> |
removed obsolete delta stuff;
|
#
6759b03d |
|
06-Jul-2005 |
wenzelm <none@none> |
multiple flags: prefer later ones;
|
#
82fed585 |
|
04-Jul-2005 |
wenzelm <none@none> |
made smlnj happy;
|
#
e74ebcf2 |
|
04-Jul-2005 |
wenzelm <none@none> |
methods: added simp_flags argument, added "depth_limit" flag;
|
#
c01306d6 |
|
17-Jun-2005 |
wenzelm <none@none> |
accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
|
#
f8eb2487 |
|
22-May-2005 |
wenzelm <none@none> |
moved here from Provers; removed find_rewrites (superceded by find_theorems rewrite); outer syntax moved to Pure/Isar/isar_syn.ML;
|