| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 14:32:26 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Tue, 20 May 2014 15:59:16 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:29:32 +0100 |
hoelzl |
fix HOL-NSA; move lemmas
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 20:04:40 +0100 |
hoelzl |
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 17:35:59 +0100 |
blanchet |
don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
remove hidden fact about hidden constant from code generator setup
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 17:14:01 +0100 |
hoelzl |
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:52 +0100 |
hoelzl |
stronger inc_induct and dec_induct
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
restructed
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
generalised lemma
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Sun, 29 Sep 2013 16:01:22 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
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
|