isabelle: File revisions

src/HOL/Tools/primrec_package.ML

2007-04-18	wenzelm	2007-04-18	simplified ProofContext.infer_types(_pats);	file \| diff \| annotate
2007-04-15	wenzelm	2007-04-15	proper ProofContext.infer_types;	file \| diff \| annotate
2007-03-20	haftmann	2007-03-20	switched exception from arbitrary to undefined	file \| diff \| annotate
2007-01-19	wenzelm	2007-01-19	moved parts of OuterParse to SpecParse;	file \| diff \| annotate
2006-10-20	haftmann	2006-10-20	fold cleanup	file \| diff \| annotate
2006-10-13	berghofe	2006-10-13	Moved old inductive package to old_inductive_package.ML	file \| diff \| annotate
2006-10-02	haftmann	2006-10-02	added gen_primrec	file \| diff \| annotate
2006-07-21	haftmann	2006-07-21	exported equation transformator	file \| diff \| annotate
2006-07-08	wenzelm	2006-07-08	Goal.prove_global;	file \| diff \| annotate
2006-05-20	wenzelm	2006-05-20	added syntax for 'unchecked';	file \| diff \| annotate
2006-05-13	wenzelm	2006-05-13	added add_primrec_unchecked_i;	file \| diff \| annotate
2006-02-15	wenzelm	2006-02-15	removed distinct, renamed gen_distinct to distinct;	file \| diff \| annotate
2006-02-07	wenzelm	2006-02-07	renamed gen_duplicates to duplicates;	file \| diff \| annotate
2006-02-06	haftmann	2006-02-06	subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate	file \| diff \| annotate
2006-01-21	wenzelm	2006-01-21	simplified type attribute;	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	generic attributes;	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	sane ERROR handling;	file \| diff \| annotate
2005-12-09	haftmann	2005-12-09	oriented result pairs in PureThy	file \| diff \| annotate
2005-12-06	haftmann	2005-12-06	removed thms 'swap' and 'nth_map' from ML toplevel	file \| diff \| annotate
2005-12-06	haftmann	2005-12-06	re-oriented some result tuples in PureThy	file \| diff \| annotate
2005-10-25	wenzelm	2005-10-25	avoid legacy goals;	file \| diff \| annotate
2005-10-21	wenzelm	2005-10-21	OldGoals;	file \| diff \| annotate
2005-09-15	wenzelm	2005-09-15	TableFun/Symtab: curried lookup and update;	file \| diff \| annotate
2005-09-08	haftmann	2005-09-08	introduces some modern-style AList operations	file \| diff \| annotate
2005-09-05	wenzelm	2005-09-05	curried_lookup/update;	file \| diff \| annotate
2005-08-29	wenzelm	2005-08-29	use AList operations;	file \| diff \| annotate
2005-08-16	wenzelm	2005-08-16	OuterKeyword;	file \| diff \| annotate
2005-07-08	berghofe	2005-07-08	Some changes to allow mutually recursive, overloaded functions with same name.	file \| diff \| annotate
2005-07-01	berghofe	2005-07-01	Adapted to new interface of RecfunCodegen.add.	file \| diff \| annotate
2005-04-13	wenzelm	2005-04-13	* MESSAGE REFERS TO PREVIOUS VERSION * Attrib.src;	file \| diff \| annotate
2005-04-13	wenzelm	2005-04-13	* empty log message *	file \| diff \| annotate
2005-03-04	skalberg	2005-03-04	Removed practically all references to Library.foldr.	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2004-06-21	kleing	2004-06-21	Merged in license change from Isabelle2004	file \| diff \| annotate
2004-05-21	wenzelm	2004-05-21	tuned message;	file \| diff \| annotate
2003-11-18	berghofe	2003-11-18	Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors.	file \| diff \| annotate
2002-10-10	berghofe	2002-10-10	Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.	file \| diff \| annotate
2002-02-12	wenzelm	2002-02-12	got rid of explicit marginal comments (now stripped earlier from input);	file \| diff \| annotate
2001-12-12	berghofe	2001-12-12	Improved error messages.	file \| diff \| annotate
2001-12-10	berghofe	2001-12-10	Recursive equations to be used for code generation are now registered via RecfunCodegen.add	file \| diff \| annotate
2001-11-28	wenzelm	2001-11-28	theory data: removed obsolete finish method;	file \| diff \| annotate
2001-11-14	wenzelm	2001-11-14	store original simps for codegen;	file \| diff \| annotate
2001-11-08	wenzelm	2001-11-08	theory data: finish method;	file \| diff \| annotate
2001-10-18	wenzelm	2001-10-18	GPLed;	file \| diff \| annotate
2001-08-31	wenzelm	2001-08-31	tuned headers;	file \| diff \| annotate
2000-11-28	wenzelm	2000-11-28	RuleCases.save;	file \| diff \| annotate
2000-08-10	berghofe	2000-08-10	Equations that are added to the simpset now have proper names.	file \| diff \| annotate
2000-07-13	wenzelm	2000-07-13	adapted PureThy.add_defs_i;	file \| diff \| annotate
2000-05-25	paulson	2000-05-25	improved error msgs, listing variable names	file \| diff \| annotate
2000-03-15	berghofe	2000-03-15	Added new theory data slot for primrec equations.	file \| diff \| annotate
2000-03-13	wenzelm	2000-03-13	adapted to new PureThy.add_thms etc.; prepare induct rule (case names);	file \| diff \| annotate
1999-10-21	wenzelm	1999-10-21	proper handling of axioms / defs;	file \| diff \| annotate
1999-10-05	berghofe	1999-10-05	Got rid of readtm.	file \| diff \| annotate
1999-09-20	berghofe	1999-09-20	Fixed bug in add_primrec which caused non-informative error message.	file \| diff \| annotate
1999-08-02	wenzelm	1999-08-02	tuned outer syntax;	file \| diff \| annotate
1999-07-16	berghofe	1999-07-16	- Now also supports arbitrarily branching datatypes. - Fixed bug (in some rare cases, recursive constants were inconsistently typed in different primrec equations).	file \| diff \| annotate
1999-05-25	wenzelm	1999-05-25	formal comments (still dummy);	file \| diff \| annotate
1999-05-24	wenzelm	1999-05-24	outer syntax keyword classification; no open OuterParse;	file \| diff \| annotate
1999-04-14	wenzelm	1999-04-14	triple_swap;	file \| diff \| annotate

isabelle

RSS Atom