2014-03-20 wenzelm 2014-03-20 more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;
2014-03-06 wenzelm 2014-03-06 more rigid type_name demands, based on educated guesses about the tools involved here;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 proper proof context; removed historic comments;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-05-14 wenzelm 2011-05-14 modernized structure Rule_Insts;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-12 wenzelm 2011-01-12 avoid catch-all exception handler, presumably TERM was meant here;
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-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-09 wenzelm 2010-03-09 tuned -- eliminated Sign.intern_sort;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-01-13 wenzelm 2010-01-13 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-20 wenzelm 2009-10-20 eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2007-09-08 urbanc 2007-09-08 some cleaning up
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-06-13 narboux 2007-06-13 generate_fresh works even if there is no free variable in the goal
2007-05-24 narboux 2007-05-24 fix a bug : the semantics of no_asm was the opposite
2007-05-24 narboux 2007-05-24 add an option in fresh_fun_simp to prevent rewriting in assumptions
2007-05-21 narboux 2007-05-21 search bottom up to get the inner fresh fun
2007-05-21 narboux 2007-05-21 change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
2007-04-25 narboux 2007-04-25 fix sml compilation
2007-04-24 narboux 2007-04-24 update fresh_fun_simp for debugging purposes
2007-04-24 narboux 2007-04-24 adds op in front of an infix to fix SML compilation
2007-04-20 narboux 2007-04-20 modify fresh_fun_simp to ease debugging
2007-04-19 narboux 2007-04-19 add a tactic to generate fresh names