| #
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.
|