isabelle: File revisions

src/HOL/Product_Type.thy

2009-05-19	haftmann	2009-05-19	pretty printing of functional combinators for evaluation code	file \| diff \| annotate
2009-04-15	haftmann	2009-04-15	default instantiation for unit type	file \| diff \| annotate
2009-03-20	berghofe	2009-03-20	split_codegen now eta-expands terms on-the-fly.	file \| diff \| annotate
2008-11-06	nipkow	2008-11-06	added lemma	file \| diff \| annotate
2008-10-10	haftmann	2008-10-10	`code func` now just `code`	file \| diff \| annotate
2008-10-09	haftmann	2008-10-09	established canonical argument order in SML code generators	file \| diff \| annotate
2008-09-25	haftmann	2008-09-25	discontinued special treatment of op = vs. eq_class.eq	file \| diff \| annotate
2008-09-17	wenzelm	2008-09-17	back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;	file \| diff \| annotate
2008-06-10	haftmann	2008-06-10	rep_datatype command now takes list of constructors as input arguments	file \| diff \| annotate
2008-05-23	berghofe	2008-05-23	Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.	file \| diff \| annotate
2008-05-07	berghofe	2008-05-07	split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.	file \| diff \| annotate
2008-04-09	haftmann	2008-04-09	removed syntax from monad combinators; renamed mbind to scomp	file \| diff \| annotate
2008-03-29	wenzelm	2008-03-29	replaced 'ML_setup' by 'ML';	file \| diff \| annotate
2008-03-20	haftmann	2008-03-20	Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned	file \| diff \| annotate
2008-03-19	wenzelm	2008-03-19	more antiquotations; eliminated change_claset/simpset;	file \| diff \| annotate
2008-02-26	bulwahn	2008-02-26	Added useful general lemmas from the work with the HeapMonad	file \| diff \| annotate
2008-01-10	berghofe	2008-01-10	New interface for test data generators.	file \| diff \| annotate
2007-12-05	haftmann	2007-12-05	simplified infrastructure for code generator operational equality	file \| diff \| annotate
2007-11-30	haftmann	2007-11-30	more canonical attribute application	file \| diff \| annotate
2007-10-04	haftmann	2007-10-04	certificates for code generator case expressions	file \| diff \| annotate
2007-09-25	haftmann	2007-09-25	datatype interpretators for size and datatype_realizer	file \| diff \| annotate
2007-08-15	paulson	2007-08-15	ATP blacklisting is now in theory data, attribute noatp	file \| diff \| annotate
2007-08-07	haftmann	2007-08-07	split off theory Option for benefit of code generator	file \| diff \| annotate
2007-06-05	haftmann	2007-06-05	merged Code_Generator.thy into HOL.thy	file \| diff \| annotate
2007-05-09	haftmann	2007-05-09	moved recfun_codegen.ML to Code_Generator.thy	file \| diff \| annotate
2007-05-06	haftmann	2007-05-06	tuned	file \| diff \| annotate
2007-04-20	haftmann	2007-04-20	Isar definitions are now added explicitly to code theorem table	file \| diff \| annotate
2007-04-04	wenzelm	2007-04-04	ML antiquotes;	file \| diff \| annotate
2007-03-12	wenzelm	2007-03-12	syntax: proper body priorty for derived binders;	file \| diff \| annotate
2007-03-02	haftmann	2007-03-02	using "fst" "snd" for Haskell code	file \| diff \| annotate
2007-02-23	haftmann	2007-02-23	slight cleanup	file \| diff \| annotate
2006-12-27	haftmann	2006-12-27	moved code generator product setup here	file \| diff \| annotate
2006-11-22	haftmann	2006-11-22	dropped eq const	file \| diff \| annotate
2006-11-17	wenzelm	2006-11-17	more robust syntax for definition/abbreviation/notation;	file \| diff \| annotate
2006-11-13	haftmann	2006-11-13	added thy dependencies	file \| diff \| annotate
2006-11-07	wenzelm	2006-11-07	renamed 'const_syntax' to 'notation';	file \| diff \| annotate
2006-11-06	haftmann	2006-11-06	two further lemmas on split	file \| diff \| annotate
2006-10-16	haftmann	2006-10-16	moved HOL code generator setup to Code_Generator	file \| diff \| annotate
2006-09-19	haftmann	2006-09-19	added operational equality	file \| diff \| annotate
2006-08-25	paulson	2006-08-25	explicit type variables prevent empty sorts	file \| diff \| annotate
2006-08-14	haftmann	2006-08-14	simplified code generator setup	file \| diff \| annotate
2006-07-12	haftmann	2006-07-12	adaptions in codegen	file \| diff \| annotate
2006-07-08	wenzelm	2006-07-08	simprocs: no theory argument -- use simpset context instead;	file \| diff \| annotate
2006-05-16	wenzelm	2006-05-16	tuned concrete syntax -- abbreviation/const_syntax;	file \| diff \| annotate
2006-05-02	wenzelm	2006-05-02	replaced syntax/translations by abbreviation; tuned proofs; tuned;	file \| diff \| annotate
2006-03-03	nipkow	2006-03-03	changed and retracted change of location of code lemmas.	file \| diff \| annotate
2006-02-25	haftmann	2006-02-25	improved codegen bootstrap	file \| diff \| annotate
2006-02-20	haftmann	2006-02-20	slight code generator serialization improvements	file \| diff \| annotate
2006-02-14	haftmann	2006-02-14	added theory of executable rational numbers	file \| diff \| annotate
2006-02-10	haftmann	2006-02-10	improved code generator devarification	file \| diff \| annotate
2006-02-07	haftmann	2006-02-07	slight improvements in code generation	file \| diff \| annotate
2006-01-23	haftmann	2006-01-23	removed problematic keyword 'atom'	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2006-01-19	berghofe	2006-01-19	Re-inserted consts_code declaration accidentally deleted during last commit.	file \| diff \| annotate
2006-01-17	haftmann	2006-01-17	substantial improvements in code generator	file \| diff \| annotate
2005-12-29	haftmann	2005-12-29	adaptions to changes in code generator	file \| diff \| annotate
2005-12-08	wenzelm	2005-12-08	tuned proofs;	file \| diff \| annotate
2005-12-02	haftmann	2005-12-02	adjusted to improved code generator interface	file \| diff \| annotate
2005-12-01	wenzelm	2005-12-01	simprocs: static evaluation of simpset;	file \| diff \| annotate
2005-11-22	haftmann	2005-11-22	added codegenerator	file \| diff \| annotate

isabelle

RSS Atom