Fri, 01 Jun 2012 15:33:31 +0200 |
Andreas Lochbihler |
more instantiations for card_UNIV,
|
file |
diff |
annotate
|
Fri, 01 Jun 2012 14:34:46 +0200 |
Andreas Lochbihler |
simplify card_UNIV type class,
|
file |
diff |
annotate
|
Fri, 01 Jun 2012 13:52:51 +0200 |
Andreas Lochbihler |
drop redundant sort constraint
|
file |
diff |
annotate
|
Thu, 31 May 2012 17:10:43 +0200 |
Andreas Lochbihler |
tuned proofs
|
file |
diff |
annotate
|
Thu, 31 May 2012 17:04:11 +0200 |
Andreas Lochbihler |
tuned instantiations
|
file |
diff |
annotate
|
Thu, 31 May 2012 16:58:38 +0200 |
Andreas Lochbihler |
unify Card_Univ and Cardinality
|
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
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
Wed, 30 Jun 2010 16:28:13 +0200 |
haftmann |
split off Cardinality from Numeral_Type
|
file |
diff |
annotate
| base
|