| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:13 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
more robust exception handling
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 09:43:00 +0200 |
blanchet |
added compatibility function
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:31:38 +0200 |
blanchet |
added countable tactic for new-style datatypes
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:32 +0200 |
blanchet |
registered 'typerep' as countable again
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:27 +0200 |
blanchet |
commented out failing tactic (now that 'typerep' is defined using the new package
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Thu, 06 Sep 2012 08:59:50 -0700 |
huffman |
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 17:58:40 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2011 19:35:00 +0200 |
hoelzl |
to_nat is injective on arbitrary domains
|
file |
diff |
annotate
|
| Thu, 23 Jun 2011 10:07:16 -0700 |
huffman |
add countable_datatype method for proving countable class instances
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
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
|
| Thu, 09 Sep 2010 14:38:14 +0200 |
bulwahn |
changing String.literal to a type instead of a datatype
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 15:12:20 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 16:28:13 +0200 |
haftmann |
added literal and typerep instances
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:22 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 14:57:13 -0800 |
huffman |
new theory Library/Nat_Bijection.thy
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 09:20:18 +0100 |
haftmann |
adjusted to cs. e4a7947e02b8
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 17:21:51 +0100 |
hoelzl |
Remove map_compose, replaced by map_map
|
file |
diff |
annotate
|