| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:21 +0200 |
blanchet |
killed more "no_atp"s
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:07:29 +0100 |
bulwahn |
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
tailored enum specification towards simple instantiation;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
refined internal structure of Enum.thy
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 16:03:21 +0200 |
bulwahn |
some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:25:34 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:22:17 +0200 |
wenzelm |
tuned proofs, less guesswork;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:00:18 +0200 |
huffman |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:24 +0100 |
bulwahn |
adding code equations for max_extp and mlex
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:22 +0100 |
bulwahn |
adding code equation for rtranclp in Enum
|
file |
diff |
annotate
|