summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
Also removed some functions that are not used any more.

improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion

reimplement copy_def to use data constructor constants

cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple

generate lambda pattern syntax for new data constructors

changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF

add constant one_when; LAM pattern for ONE

add translation for wildcard pattern

change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

Thu, 03 Nov 2005 01:02:29 +0100
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1