isabelle: File revisions

src/Pure/simplifier.ML

2009-09-30	wenzelm	2009-09-30	eliminated dead code;	file \| diff \| annotate
2009-09-29	wenzelm	2009-09-29	explicit indication of Unsynchronized.ref;	file \| diff \| annotate
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;	file \| diff \| annotate
2009-07-21	wenzelm	2009-07-21	proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;	file \| diff \| annotate
2009-05-30	wenzelm	2009-05-30	modernized method setup; tuned;	file \| diff \| annotate
2009-03-20	wenzelm	2009-03-20	Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;	file \| diff \| annotate
2009-03-15	wenzelm	2009-03-15	simplified attribute setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	eliminated type Args.T; pervasive types 'a parser and 'a context_parser;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	unified type Proof.method and pervasive METHOD combinators;	file \| diff \| annotate
2009-03-12	wenzelm	2009-03-12	renamed NameSpace.bind to NameSpace.define;	file \| diff \| annotate
2009-03-08	wenzelm	2009-03-08	added dest_ss; proper context fo pretty_ss; tuned;	file \| diff \| annotate
2009-03-07	wenzelm	2009-03-07	renamed rep_ss to MetaSimplifier.internal_ss;	file \| diff \| annotate
2009-01-21	wenzelm	2009-01-21	removed Ids;	file \| diff \| annotate
2008-12-05	haftmann	2008-12-05	dropped NameSpace.declare_base	file \| diff \| annotate
2008-12-04	haftmann	2008-12-04	cleaned up binding module and related code	file \| diff \| annotate
2008-11-20	haftmann	2008-11-20	dropped legacy naming code	file \| diff \| annotate
2008-11-14	haftmann	2008-11-14	namify and name_decl combinators	file \| diff \| annotate
2008-11-13	haftmann	2008-11-13	consider prefixes for name bindings of simprocs (a first approximation)	file \| diff \| annotate
2008-09-02	wenzelm	2008-09-02	name/var morphism operates on Name.binding;	file \| diff \| annotate
2008-06-24	wenzelm	2008-06-24	ML_Antiquote.value;	file \| diff \| annotate
2008-05-29	wenzelm	2008-05-29	proper context for attribute simplified;	file \| diff \| annotate
2008-04-15	wenzelm	2008-04-15	Thm.forall_elim_var(s);	file \| diff \| annotate
2008-03-29	wenzelm	2008-03-29	purely functional setup of claset/simpset/clasimpset; tuned signature;	file \| diff \| annotate
2008-03-28	wenzelm	2008-03-28	Context.>> : operate on Context.generic;	file \| diff \| annotate
2008-03-27	wenzelm	2008-03-27	eliminated delayed theory setup	file \| diff \| annotate
2008-03-27	wenzelm	2008-03-27	renamed ML_Context.the_context to ML_Context.the_global_context;	file \| diff \| annotate
2007-09-01	wenzelm	2007-09-01	replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);	file \| diff \| annotate
2007-08-02	wenzelm	2007-08-02	turned simp_depth_limit into configuration option;	file \| diff \| annotate
2007-07-28	wenzelm	2007-07-28	added attribute "simproc"; marked some CRITICAL sections; tuned;	file \| diff \| annotate
2007-07-08	wenzelm	2007-07-08	replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;	file \| diff \| annotate
2007-07-05	wenzelm	2007-07-05	tuned;	file \| diff \| annotate
2007-07-03	wenzelm	2007-07-03	moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);	file \| diff \| annotate
2007-05-24	haftmann	2007-05-24	tuned Pure/General/name_space.ML	file \| diff \| annotate
2007-05-07	wenzelm	2007-05-07	simplified DataFun interfaces;	file \| diff \| annotate
2007-04-23	wenzelm	2007-04-23	def_simproc(_i): proper ProofContext.read/cert_terms;	file \| diff \| annotate
2007-04-16	haftmann	2007-04-16	canonical merge operations	file \| diff \| annotate
2007-04-15	wenzelm	2007-04-15	removed obsolete TypeInfer.logicT -- use dummyT;	file \| diff \| annotate
2007-02-28	wenzelm	2007-02-28	exported get_ss, map_ss;	file \| diff \| annotate
2007-02-04	wenzelm	2007-02-04	def_simproc(_i): tuned interface; tuned simprocs environment;	file \| diff \| annotate
2007-01-29	wenzelm	2007-01-29	added get_simproc, @{simproc};	file \| diff \| annotate
2007-01-28	wenzelm	2007-01-28	added def_simproc(_i) -- define named simprocs; tuned;	file \| diff \| annotate
2007-01-20	wenzelm	2007-01-20	added @{simpset};	file \| diff \| annotate
2007-01-19	wenzelm	2007-01-19	moved ML context stuff to from Context to ML_Context;	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-11-10	haftmann	2006-11-10	introduces canonical AList functions for loop_tacs	file \| diff \| annotate
2006-10-07	wenzelm	2006-10-07	tuned;	file \| diff \| annotate
2006-02-10	wenzelm	2006-02-10	Args/Attrib syntax: Context.generic;	file \| diff \| annotate
2006-01-21	wenzelm	2006-01-21	simplified type attribute;	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	generic attributes;	file \| diff \| annotate
2006-01-10	wenzelm	2006-01-10	Attrib.rule;	file \| diff \| annotate
2005-10-28	wenzelm	2005-10-28	export cong_modifiers, simp_modifiers';	file \| diff \| annotate
2005-10-21	wenzelm	2005-10-21	added simplification tactics and rules (from meta_simplifier.ML);	file \| diff \| annotate
2005-10-18	wenzelm	2005-10-18	renamed set_context to context; data extend: reset context;	file \| diff \| annotate
2005-10-17	wenzelm	2005-10-17	removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;	file \| diff \| annotate
2005-09-29	wenzelm	2005-09-29	export debug_bounds;	file \| diff \| annotate
2005-08-02	wenzelm	2005-08-02	export clear_ss;	file \| diff \| annotate
2005-08-01	wenzelm	2005-08-01	export MataSimplifier.inherit_bounds;	file \| diff \| annotate
2005-07-13	wenzelm	2005-07-13	removed obsolete delta stuff;	file \| diff \| annotate

isabelle

RSS Atom