isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/HOL/Option.thy

2012-09-07	haftmann	combinator Option.these	file \| diff \| annotate
2012-02-18	krauss	added congruence rules for Option.{map\|bind}	file \| diff \| annotate
2011-01-11	haftmann	"enriched_type" replaces less specific "type_lifting"	file \| diff \| annotate
2010-12-21	haftmann	tuned type_lifting declarations	file \| diff \| annotate
2010-12-06	haftmann	replace `type_mapper` by the more adequate `type_lifting`	file \| diff \| annotate
2010-11-18	haftmann	mapper for option type	file \| diff \| annotate
2010-09-10	haftmann	Haskell == is infix, not infixl	file \| diff \| annotate
2010-09-06	wenzelm	more antiquotations;	file \| diff \| annotate
2010-09-05	krauss	removed duplicate lemma	file \| diff \| annotate
2010-09-05	krauss	added Option.bind	file \| diff \| annotate
2010-08-27	haftmann	renamed class/constant eq to equal; tuned some instantiations	file \| diff \| annotate
2010-07-19	haftmann	Scala: subtle difference in printing strings vs. complex mixfix syntax	file \| diff \| annotate
2010-04-16	wenzelm	replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;	file \| diff \| annotate
2010-03-10	haftmann	split off theory Big_Operators from theory Finite_Set	file \| diff \| annotate
2010-01-13	haftmann	some syntax setup for Scala	file \| diff \| annotate
2009-07-14	haftmann	prefer code_inline over code_unfold; use code_unfold_post where appropriate	file \| diff \| annotate
2009-07-14	haftmann	code attributes use common underscore convention	file \| diff \| annotate
2009-05-14	haftmann	preprocessing must consider eq	file \| diff \| annotate
2009-05-09	nipkow	lemmas by Andreas Lochbihler	file \| diff \| annotate
2009-03-06	haftmann	moved instance option :: finite to Option.thy	file \| diff \| annotate
2009-03-04	nipkow	Option.thy	file \| diff \| annotate
2007-08-07	haftmann	split off Option theory	file \| diff \| annotate
2000-05-30	berghofe	the is now defined using primrec, avoiding explicit use of arbitrary.	file \| diff \| annotate
1998-09-09	oheimb	AddIffs[not_None_eq];	file \| diff \| annotate
1998-07-24	berghofe	Adapted to new datatype package.	file \| diff \| annotate
1998-03-24	oheimb	added o2s	file \| diff \| annotate
1997-11-10	oheimb	replaced 8bit characters	file \| diff \| annotate
1997-11-04	oheimb	added the, option_map, and case analysis theorems	file \| diff \| annotate
1996-09-24	nipkow	Moved Option out of IOA into core HOL	file \| diff \| annotate

less more (0) tip

isabelle

RSS Atom