isabelle: File revisions

src/HOL/Code_Setup.thy

2009-03-16	wenzelm	2009-03-16	simplified method setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	unified type Proof.method and pervasive METHOD combinators;	file \| diff \| annotate
2008-12-15	haftmann	2008-12-15	moved value.ML to src/Tools	file \| diff \| annotate
2008-11-20	wenzelm	2008-11-20	Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;	file \| diff \| annotate
2008-11-13	haftmann	2008-11-13	improved handling of !!/==> for eval and normalization	file \| diff \| annotate
2008-10-28	ballarin	2008-10-28	Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.	file \| diff \| annotate
2008-10-24	haftmann	2008-10-24	simplified syntax for class parameters	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-10-07	haftmann	2008-10-07	corrected SML undefined	file \| diff \| annotate
2008-09-29	haftmann	2008-09-29	polished code generator setup	file \| diff \| annotate
2008-09-25	haftmann	2008-09-25	discontinued special treatment of op = vs. eq_class.eq	file \| diff \| annotate
2008-09-18	wenzelm	2008-09-18	simplified oracle interface;	file \| diff \| annotate
2008-08-28	haftmann	2008-08-28	restructured and split code serializer module	file \| diff \| annotate
2008-08-27	haftmann	2008-08-27	tuned code generator setup	file \| diff \| annotate
2008-07-03	haftmann	2008-07-03	adjusted postprocessort setup	file \| diff \| annotate
2008-06-10	haftmann	2008-06-10	major refactorings in code generator modules	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-01-25	haftmann	2008-01-25	clarified setup of method "normalization"	file \| diff \| annotate
2008-01-15	haftmann	2008-01-15	explicit code lemma for implication	file \| diff \| annotate
2008-01-10	berghofe	2008-01-10	New interface for test data generators.	file \| diff \| annotate
2008-01-08	haftmann	2008-01-08	normalization conversion	file \| diff \| annotate
2008-01-08	berghofe	2008-01-08	imp_conv_disj is now declared as a "code unfold" lemma to avoid that conclusion is evaluated eagerly.	file \| diff \| annotate
2007-12-05	haftmann	2007-12-05	simplified infrastructure for code generator operational equality	file \| diff \| annotate
2007-10-04	haftmann	2007-10-04	certificates for code generator case expressions	file \| diff \| annotate
2007-10-04	haftmann	2007-10-04	clarified relationship of code generator conversions and evaluations	file \| diff \| annotate
2007-08-28	berghofe	2007-08-28	Smaller size and fewer iterations for quickcheck.	file \| diff \| annotate
2007-08-16	haftmann	2007-08-16	fixed codegen setup	file \| diff \| annotate
2007-08-15	haftmann	2007-08-15	added Code_Setup	file \| diff \| annotate

isabelle

RSS Atom