isabelle: File revisions

src/Pure/tactic.ML

2013-04-03	wenzelm	2013-04-03	tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);	file \| diff \| annotate
2012-11-26	wenzelm	2012-11-26	tuned signature; tuned;	file \| diff \| annotate
2012-11-11	wenzelm	2012-11-11	tuned;	file \| diff \| annotate
2012-10-16	wenzelm	2012-10-16	clarified defer/prefer: more specific errors;	file \| diff \| annotate
2012-02-27	wenzelm	2012-02-27	simplified cut_tac (cf. d549b5b0f344);	file \| diff \| annotate
2012-02-14	wenzelm	2012-02-14	eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);	file \| diff \| annotate
2012-02-14	wenzelm	2012-02-14	eliminated obsolete aliases;	file \| diff \| annotate
2011-04-08	wenzelm	2011-04-08	discontinued special treatment of structure Lexicon;	file \| diff \| annotate
2010-05-15	wenzelm	2010-05-15	less pervasive names from structure Thm;	file \| diff \| annotate
2010-04-30	wenzelm	2010-04-30	proper context for rule_by_tactic;	file \| diff \| annotate
2010-04-26	wenzelm	2010-04-26	eliminanated some unreferenced identifiers; tuned;	file \| diff \| annotate
2010-03-06	wenzelm	2010-03-06	removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);	file \| diff \| annotate
2009-11-25	haftmann	2009-11-25	normalized uncurry take/drop	file \| diff \| annotate
2009-11-24	haftmann	2009-11-24	curried take/drop	file \| diff \| annotate
2009-10-17	wenzelm	2009-10-17	less pervasive names;	file \| diff \| annotate
2009-07-06	wenzelm	2009-07-06	structure Thm: less pervasive names;	file \| diff \| annotate
2009-06-24	wenzelm	2009-06-24	renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);	file \| diff \| annotate
2009-05-24	haftmann	2009-05-24	tuned whitespace	file \| diff \| annotate
2009-03-17	wenzelm	2009-03-17	renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);	file \| diff \| annotate
2008-12-31	wenzelm	2008-12-31	qualified Term.rename_wrt_term;	file \| diff \| annotate
2008-06-16	wenzelm	2008-06-16	removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;	file \| diff \| annotate
2008-06-14	wenzelm	2008-06-14	qualified old res_inst_tac variants;	file \| diff \| annotate
2008-06-11	wenzelm	2008-06-11	Drule.read_instantiate; Drule.types_sorts;	file \| diff \| annotate
2008-04-12	wenzelm	2008-04-12	rep_cterm/rep_thm: no longer dereference theory_ref;	file \| diff \| annotate
2008-03-27	wenzelm	2008-03-27	eliminated theory ProtoPure;	file \| diff \| annotate
2008-01-21	berghofe	2008-01-21	Removed Logic.auto_rename.	file \| diff \| annotate
2007-08-13	wenzelm	2007-08-13	Lexicon.read_indexname/nat/variable;	file \| diff \| annotate
2007-07-03	wenzelm	2007-07-03	removed obsolete eta_long_tac;	file \| diff \| annotate
2007-06-25	wenzelm	2007-06-25	added eta_long_tac;	file \| diff \| annotate
2007-06-03	wenzelm	2007-06-03	cleaned up signature;	file \| diff \| annotate
2007-05-31	wenzelm	2007-05-31	simplified/unified list fold;	file \| diff \| annotate
2007-04-04	wenzelm	2007-04-04	added scanwords from library.ML (for obsolete rename_tac);	file \| diff \| annotate
2007-04-03	wenzelm	2007-04-03	renamed Variable.import to import_thms (avoid clash with Alice keywords);	file \| diff \| annotate
2007-04-02	paulson	2007-04-02	now exports distinct_subgoal_tac (needed by MetisAPI)	file \| diff \| annotate
2007-02-26	wenzelm	2007-02-26	moved eq_thm etc. to structure Thm in Pure/more_thm.ML;	file \| diff \| annotate
2006-12-07	wenzelm	2006-12-07	reorganized structure Tactic vs. MetaSimplifier;	file \| diff \| annotate
2006-12-07	wenzelm	2006-12-07	reorganized structure Goal vs. Tactic;	file \| diff \| annotate
2006-08-02	wenzelm	2006-08-02	renamed Syntax.indexname to Syntax.read_indexname;	file \| diff \| annotate
2006-07-27	wenzelm	2006-07-27	removed obsolete is_fact (cf. Thm.no_prems);	file \| diff \| annotate
2006-07-26	wenzelm	2006-07-26	Variable.import(T): result includes fixed types/terms;	file \| diff \| annotate
2006-07-12	wenzelm	2006-07-12	exported make_elim_preserve;	file \| diff \| annotate
2006-06-19	wenzelm	2006-06-19	eliminated freeze/varify in favour of Variable.import/export/trade;	file \| diff \| annotate
2006-05-29	paulson	2006-05-29	fixing a variable-clash bug in rule_by_tactic	file \| diff \| annotate
2006-05-02	paulson	2006-05-02	tidied and harmonized "params_of_state"	file \| diff \| annotate
2006-04-27	wenzelm	2006-04-27	tuned basic list operators (flat, maps, map_filter);	file \| diff \| annotate
2006-04-26	wenzelm	2006-04-26	tuned;	file \| diff \| annotate
2006-04-13	wenzelm	2006-04-13	use conjunction stuff from conjunction.ML;	file \| diff \| annotate
2006-03-04	wenzelm	2006-03-04	tuned conj_curry;	file \| diff \| annotate
2006-02-22	wenzelm	2006-02-22	simplified Pure conjunction, based on actual const;	file \| diff \| annotate
2006-02-15	wenzelm	2006-02-15	sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;	file \| diff \| annotate
2006-02-08	haftmann	2006-02-08	introduced gen_distinct in place of distinct	file \| diff \| annotate
2005-12-23	wenzelm	2005-12-23	CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;	file \| diff \| annotate
2005-12-22	wenzelm	2005-12-22	conjunction_tac: single goal; added CONJUNCTS2, precise_conjunction_tac; removed smart_conjunction_tac;	file \| diff \| annotate
2005-11-19	wenzelm	2005-11-19	added CONJUNCTS: treat conjunction as separate sub-goals;	file \| diff \| annotate
2005-11-10	wenzelm	2005-11-10	renamed Thm.cgoal_of to Thm.cprem_of;	file \| diff \| annotate
2005-10-28	wenzelm	2005-10-28	accomodate simplified Thm.lift_rule; tuned;	file \| diff \| annotate
2005-10-21	wenzelm	2005-10-21	moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;	file \| diff \| annotate
2005-10-18	wenzelm	2005-10-18	Simplifier.theory_context;	file \| diff \| annotate
2005-10-15	wenzelm	2005-10-15	tuned comments;	file \| diff \| annotate
2005-09-20	haftmann	2005-09-20	slight adaptions to library changes	file \| diff \| annotate

isabelle

RSS Atom