| Thu, 07 Feb 2008 14:39:19 +0100 |
berghofe |
Instead of raising an exception, pred_set_conv now ignores conversion
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 17:08:36 +0100 |
wenzelm |
added theorem group;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 14:56:38 +0100 |
berghofe |
to_set now applies collect_mem_simproc as well.
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 10:50:33 +0100 |
berghofe |
to_pred and to_set now save induction and case rule tags.
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:39 +0200 |
wenzelm |
renamed LocalTheory.def to LocalTheory.define;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:32 +0200 |
wenzelm |
removed LocalTheory.defs, use plain LocalTheory.def;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Tue, 02 Oct 2007 22:23:26 +0200 |
wenzelm |
tuned internal interfaces: flags record, added kind for results;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2007 10:30:51 +0200 |
berghofe |
add_inductive_i now takes typ instead of typ option as argument.
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 15:37:37 +0200 |
berghofe |
strong_ind_simproc now only rewrites arguments of inductive predicates.
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:43:31 +0200 |
berghofe |
New wrapper for defining inductive sets with new inductive
|
file |
diff |
annotate
|