src/Pure/assumption.ML
2014-12-19 wenzelm 2014-12-19 tuned;
2014-01-10 wenzelm 2014-01-10 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;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-11-23 wenzelm 2013-11-23 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;
2012-03-31 wenzelm 2012-03-31 tuned comment;
2012-02-15 wenzelm 2012-02-15 discontinued obsolete "prems" fact;
2011-11-27 wenzelm 2011-11-27 tuned;
2011-10-28 wenzelm 2011-10-28 slightly more explicit/syntactic modelling of morphisms;
2011-01-14 wenzelm 2011-01-14 global "prems" is legacy feature;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-03-11 wenzelm 2010-03-11 tuned signature;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-03-12 wenzelm 2009-03-12 tuned;
2009-03-12 wenzelm 2009-03-12 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;
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-25 wenzelm 2008-03-25 setup for dynamic "prems" (legacy);
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation; tuned export_morphism -- lean closure;
2006-11-30 wenzelm 2006-11-30 qualified MetaSimplifier.norm_hhf(_protect);
2006-11-29 wenzelm 2006-11-29 assms_of: cterm;
2006-11-24 wenzelm 2006-11-24 added export_morphism;
2006-08-02 wenzelm 2006-08-02 simplified export: no Seq.seq; normalized Proof.context/method type aliases;
2006-07-27 wenzelm 2006-07-27 Local assumptions, parameterized by export rules.