haftmann [Mon, 07 Nov 2005 11:39:24 +0100] rev 18102
added fillin_mixfix, replace_quote
berghofe [Mon, 07 Nov 2005 11:28:34 +0100] rev 18101
New function store_thmss_atts.
urbanc [Mon, 07 Nov 2005 11:17:45 +0100] rev 18100
used the function Library.product for the cprod from Stefan
urbanc [Mon, 07 Nov 2005 10:47:25 +0100] rev 18099
fixed bug with nominal induct
- the bug occured in rule inductions when
the goal did not use all variables from
the relation over which the induction
was done
haftmann [Mon, 07 Nov 2005 09:34:51 +0100] rev 18098
added fillin_mixfix' needed by serializer
huffman [Sun, 06 Nov 2005 01:21:37 +0100] rev 18097
add case syntax stuff
huffman [Sun, 06 Nov 2005 00:35:24 +0100] rev 18096
use consts for infix syntax
huffman [Sun, 06 Nov 2005 00:22:03 +0100] rev 18095
add proof of Bekic's theorem: fix_cprod
huffman [Sat, 05 Nov 2005 21:56:45 +0100] rev 18094
simplify definitions
huffman [Sat, 05 Nov 2005 21:52:13 +0100] rev 18093
put iterate and fix in separate sections; added Letrec
huffman [Sat, 05 Nov 2005 21:50:37 +0100] rev 18092
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman [Sat, 05 Nov 2005 21:42:24 +0100] rev 18091
add line breaks to Rep_CFun syntax
huffman [Fri, 04 Nov 2005 23:15:45 +0100] rev 18090
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman [Fri, 04 Nov 2005 23:15:11 +0100] rev 18089
moved adm_chfindom from Fix.thy to Cfun.thy
huffman [Fri, 04 Nov 2005 22:27:40 +0100] rev 18088
cleaned up
huffman [Fri, 04 Nov 2005 22:26:09 +0100] rev 18087
add print translation: Abs_CFun f => LAM x. f x
mengj [Thu, 03 Nov 2005 04:31:12 +0100] rev 18086
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.
huffman [Thu, 03 Nov 2005 03:06:02 +0100] rev 18085
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
huffman [Thu, 03 Nov 2005 02:37:09 +0100] rev 18084
reimplement copy_def to use data constructor constants
huffman [Thu, 03 Nov 2005 02:19:48 +0100] rev 18083
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
huffman [Thu, 03 Nov 2005 01:54:51 +0100] rev 18082
generate lambda pattern syntax for new data constructors
huffman [Thu, 03 Nov 2005 01:45:52 +0100] rev 18081
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
huffman [Thu, 03 Nov 2005 01:44:27 +0100] rev 18080
add constant one_when; LAM pattern for ONE
huffman [Thu, 03 Nov 2005 01:28:22 +0100] rev 18079
add translation for wildcard pattern
huffman [Thu, 03 Nov 2005 01:11:39 +0100] rev 18078
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman [Thu, 03 Nov 2005 01:02:29 +0100] rev 18077
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman [Thu, 03 Nov 2005 00:57:35 +0100] rev 18076
cleaned up; ch2ch_Rep_CFun is a simp rule
huffman [Thu, 03 Nov 2005 00:43:50 +0100] rev 18075
changed iterate to a continuous type