| Wed, 30 Mar 2011 11:32:52 +0200 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Sun, 10 Oct 2010 22:50:25 +0200 |
krauss |
removed output syntax "'a ~=> 'b" for "'a => 'b option"
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:43:23 +0200 |
haftmann |
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:31:31 +0100 |
haftmann |
lemma restrict_complement_singleton_eq
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 09:58:30 +0100 |
haftmann |
added dom_option_map, map_of_map_keys
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 11:22:06 +0100 |
haftmann |
lemmas set_map_of_compr, map_of_inject_set
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 20:45:48 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 20:45:31 +0100 |
haftmann |
more uniform naming conventions
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 23:59:54 +0100 |
wenzelm |
proper (type_)notation;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 09:48:53 +0100 |
haftmann |
added lemma map_of_map_restrict; generalized lemma dom_const
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Sun, 31 Jan 2010 14:51:32 +0100 |
haftmann |
more correspondence lemmas between related operations
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 15:10:24 +0100 |
haftmann |
moved lemma map_of_zip_map to Map.thy
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 22:50:01 +0200 |
krauss |
some lemmas about maps (contributed by Peter Lammich)
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 16:23:43 +0200 |
haftmann |
added/moved lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 14:02:12 +0200 |
haftmann |
dropped unnamed infix
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Fri, 23 Jan 2009 19:51:48 +0100 |
haftmann |
lemmas dom_const, dom_if
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:08 +0100 |
haftmann |
lemmas about dom and minus / insert
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:04:37 +0100 |
haftmann |
lemmas about map_of (zip _ _)
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:01:51 +0100 |
haftmann |
whitespace typo
|
file |
diff |
annotate
|