isabelle: File revisions

src/Pure/proofterm.ML

2005-04-21	berghofe	2005-04-21	- Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.	file \| diff \| annotate
2005-03-26	gagern	2005-03-26	op vor infix-Konstruktoren im datatype binding zum besseren Parsen	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-07-09	berghofe	2004-07-09	- Expressed infer_derivs' in terms of infer_deriv - Eta-expanded function instantiate to delay evaluation (avoids inefficiencies when proof terms are switched off)	file \| diff \| annotate
2004-06-21	kleing	2004-06-21	Merged in license change from Isabelle2004	file \| diff \| annotate
2004-06-01	wenzelm	2004-06-01	removed obsolete sort 'logic';	file \| diff \| annotate
2004-05-21	wenzelm	2004-05-21	adapted tsig interface;	file \| diff \| annotate
2002-12-13	berghofe	2002-12-13	size_of_proof no longer includes size_of_term	file \| diff \| annotate
2002-12-10	berghofe	2002-12-10	Added size_of_proof.	file \| diff \| annotate
2002-10-21	berghofe	2002-10-21	Removed Logic.strip_flexpairs.	file \| diff \| annotate
2002-10-07	nipkow	2002-10-07	take/drop -> splitAt	file \| diff \| annotate
2002-08-27	wenzelm	2002-08-27	thms/axms_of_proof: proper handling of MinProof;	file \| diff \| annotate
2002-05-04	berghofe	2002-05-04	Added skeletons to speed up rewriting on proof terms.	file \| diff \| annotate
2002-02-21	wenzelm	2002-02-21	fixed get_name_tags in order to work with hyps;	file \| diff \| annotate
2002-02-20	berghofe	2002-02-20	New function change_type for changing type assignments of theorems, axioms and oracles.	file \| diff \| annotate
2002-02-14	wenzelm	2002-02-14	made MLWorks happy;	file \| diff \| annotate
2002-02-06	berghofe	2002-02-06	Added function could_unify to speed up rewriting of proof terms.	file \| diff \| annotate
2002-02-05	berghofe	2002-02-05	New function maxidx_of_proof.	file \| diff \| annotate
2001-12-14	wenzelm	2001-12-14	type_env;	file \| diff \| annotate
2001-11-28	wenzelm	2001-11-28	theory data: removed obsolete finish method;	file \| diff \| annotate
2001-11-24	wenzelm	2001-11-24	fixed SML/NJ error (!?);	file \| diff \| annotate
2001-11-24	wenzelm	2001-11-24	use merge_lists, merge_alists;	file \| diff \| annotate
2001-11-24	berghofe	2001-11-24	Extended match_proof to handle abstractions.	file \| diff \| annotate
2001-11-19	berghofe	2001-11-19	- Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data	file \| diff \| annotate
2001-11-09	wenzelm	2001-11-09	theory data: finish method;	file \| diff \| annotate
2001-11-03	berghofe	2001-11-03	Fixed bug in function add_npvars.	file \| diff \| annotate
2001-10-31	berghofe	2001-10-31	Tuned function thm_proof.	file \| diff \| annotate
2001-10-10	berghofe	2001-10-10	Tuned several functions to improve sharing of unchanged subproofs.	file \| diff \| annotate
2001-10-03	paulson	2001-10-03	eta-expansion required for SML/NJ	file \| diff \| annotate
2001-09-28	berghofe	2001-09-28	- Exchanged % and %%. - Fixed bug in shrink.	file \| diff \| annotate
2001-09-01	wenzelm	2001-09-01	renamed `keep_derivs' to `proofs', and made an integer;	file \| diff \| annotate
2001-08-31	wenzelm	2001-08-31	fixed header;	file \| diff \| annotate
2001-08-31	berghofe	2001-08-31	New implementation of LF style proof terms.	file \| diff \| annotate

isabelle

RSS Atom