isabelle: File revisions

src/HOL/Tools/datatype_realizer.ML

2006-08-02	wenzelm	2006-08-02	removed obsolete Drule.frees/vars_of etc.;	file \| diff \| annotate
2006-07-11	wenzelm	2006-07-11	replaced Term.variant(list) by Name.variant(_list);	file \| diff \| annotate
2006-06-07	wenzelm	2006-06-07	renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;	file \| diff \| annotate
2006-02-06	wenzelm	2006-02-06	Envir.(beta_)eta_contract;	file \| diff \| annotate
2005-12-06	haftmann	2005-12-06	re-oriented some result tuples in PureThy	file \| diff \| annotate
2005-10-21	wenzelm	2005-10-21	OldGoals;	file \| diff \| annotate
2005-09-20	haftmann	2005-09-20	introduced AList module in favor of assoc etc.	file \| diff \| annotate
2005-05-31	wenzelm	2005-05-31	Theory.restore_naming;	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-10-26	berghofe	2004-10-26	Fixed problem with sorts in function make_casedists.	file \| diff \| annotate
2004-06-21	kleing	2004-06-21	Merged in license change from Isabelle2004	file \| diff \| annotate
2002-11-27	berghofe	2002-11-27	Changed format of realizers / correctness proofs.	file \| diff \| annotate
2002-11-13	berghofe	2002-11-13	prove_goal' -> Goal.simple_prove_goal_cterm	file \| diff \| annotate
2002-10-21	berghofe	2002-10-21	Changed type of Logic.strip_horn.	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-08-07	berghofe	2002-08-07	Module for defining realizers for induction and case analysis theorems for datatypes.	file \| diff \| annotate

isabelle

RSS Atom