#
577c0313 |
|
28-Nov-2019 |
wenzelm <none@none> |
more structural integrity;
|
#
5d71d361 |
|
19-Sep-2019 |
wenzelm <none@none> |
explicit check of assumption prefix;
|
#
04b63c2e |
|
03-Jun-2019 |
wenzelm <none@none> |
more structural integrity;
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
2c211c06 |
|
18-Dec-2014 |
wenzelm <none@none> |
tuned;
|
#
db965533 |
|
10-Jan-2014 |
wenzelm <none@none> |
more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
|
#
47e6e8c3 |
|
31-Dec-2013 |
wenzelm <none@none> |
proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
|
#
116fd647 |
|
13-Dec-2013 |
wenzelm <none@none> |
maintain morphism names for diagnostic purposes;
|
#
d6996d1f |
|
23-Nov-2013 |
wenzelm <none@none> |
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
|
#
96c84f26 |
|
31-Mar-2012 |
wenzelm <none@none> |
tuned comment;
|
#
cf3fb660 |
|
15-Feb-2012 |
wenzelm <none@none> |
discontinued obsolete "prems" fact;
|
#
084f0148 |
|
27-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
4bc0a98d |
|
28-Oct-2011 |
wenzelm <none@none> |
slightly more explicit/syntactic modelling of morphisms;
|
#
a5083608 |
|
14-Jan-2011 |
wenzelm <none@none> |
global "prems" is legacy feature;
|
#
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
|
#
308c65f5 |
|
20-Sep-2010 |
wenzelm <none@none> |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; --HG-- rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML
|
#
0680143f |
|
11-Mar-2010 |
wenzelm <none@none> |
tuned signature;
|
#
02c48bf5 |
|
25-Nov-2009 |
haftmann <none@none> |
normalized uncurry take/drop --HG-- extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9
|
#
e3772a5e |
|
24-Nov-2009 |
haftmann <none@none> |
curried take/drop --HG-- extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0
|
#
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data; tuned;
|
#
5419ea4d |
|
12-Mar-2009 |
wenzelm <none@none> |
tuned;
|
#
87a1e4da |
|
12-Mar-2009 |
wenzelm <none@none> |
renamed assms_of to all_assms_of, and prems_of to all_prems_of; added local_assms_of, local_prems_of; removed unused add_view;
|
#
a6048cae |
|
21-Jan-2009 |
wenzelm <none@none> |
eliminated obsolete var morphism;
|
#
5061c2dd |
|
21-Jan-2009 |
haftmann <none@none> |
binding replaces bstring
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
55096917 |
|
28-Mar-2008 |
wenzelm <none@none> |
Context.>> : operate on Context.generic;
|
#
ebe088c1 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated delayed theory setup
|
#
b7b13c97 |
|
25-Mar-2008 |
wenzelm <none@none> |
setup for dynamic "prems" (legacy);
|
#
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
#
369e196e |
|
06-Dec-2006 |
wenzelm <none@none> |
export: added explicit term operation; tuned export_morphism -- lean closure;
|
#
87fdda9f |
|
30-Nov-2006 |
wenzelm <none@none> |
qualified MetaSimplifier.norm_hhf(_protect);
|
#
57953b59 |
|
28-Nov-2006 |
wenzelm <none@none> |
assms_of: cterm;
|
#
6c3cb4e2 |
|
24-Nov-2006 |
wenzelm <none@none> |
added export_morphism;
|
#
d5187301 |
|
02-Aug-2006 |
wenzelm <none@none> |
simplified export: no Seq.seq; normalized Proof.context/method type aliases;
|
#
4fd5b98e |
|
27-Jul-2006 |
wenzelm <none@none> |
Local assumptions, parameterized by export rules.
|