src/Pure/conjunction.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2015-07-28 wenzelm 2015-07-28 more explicit context; tuned signature;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-07-01 wenzelm 2015-07-01 support for subgoal focus command;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-04-06 wenzelm 2014-04-06 more source positions;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-10-28 wenzelm 2009-10-28 Drule.store: proper binding; conceal internal bindings;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-03-31 wenzelm 2009-03-31 added dest_conjunctions (cf. Logic.dest_conjunctions);
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-03-29 wenzelm 2008-03-29 certify wrt. dynamic context;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-10-11 wenzelm 2007-10-11 moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-08-13 wenzelm 2007-08-13 SimpleSyntax.read_prop;
2007-07-03 wenzelm 2007-07-03 removed obsolete mk_conjunction_list, intr/elim_list;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions; tuned interfaces; tuned;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-09-21 wenzelm 2006-09-21 Thm.dest_binop;
2006-09-12 wenzelm 2006-09-12 intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
2006-07-30 wenzelm 2006-07-30 Thm.adjust_maxidx;
2006-07-29 wenzelm 2006-07-29 added mk_conjunction_list;
2006-07-27 wenzelm 2006-07-27 eliminated obsolete freeze_thaw;
2006-04-13 wenzelm 2006-04-13 Meta-level conjunction.