wenzelm [Tue, 08 Nov 2005 10:43:10 +0100] rev 18119
export compose_hhf;
removed obsolete norm_hhf_plain;
tuned;
wenzelm [Tue, 08 Nov 2005 10:43:09 +0100] rev 18118
removed impose_hyps, satisfy_hyps;
tuned;
wenzelm [Tue, 08 Nov 2005 10:43:08 +0100] rev 18117
const args: do not store variable names (unused);
wenzelm [Tue, 08 Nov 2005 10:43:05 +0100] rev 18116
renamed goals.ML to old_goals.ML;
haftmann [Tue, 08 Nov 2005 09:13:22 +0100] rev 18115
(fix for accidental commit)
haftmann [Tue, 08 Nov 2005 09:12:02 +0100] rev 18114
(codegen)
huffman [Tue, 08 Nov 2005 02:19:11 +0100] rev 18113
generate pattern combinators for new datatypes
huffman [Mon, 07 Nov 2005 23:33:01 +0100] rev 18112
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
huffman [Mon, 07 Nov 2005 23:30:49 +0100] rev 18111
add case syntax for type one
huffman [Mon, 07 Nov 2005 19:23:53 +0100] rev 18110
remove syntax for as-patterns
wenzelm [Mon, 07 Nov 2005 19:03:02 +0100] rev 18109
avoid 'as' as identifier;
wenzelm [Mon, 07 Nov 2005 18:50:53 +0100] rev 18108
avoid 'as' as identifier;
berghofe [Mon, 07 Nov 2005 18:32:54 +0100] rev 18107
Added strong induction theorem (currently only axiomatized!).
urbanc [Mon, 07 Nov 2005 15:19:03 +0100] rev 18106
Initial commit.
urbanc [Mon, 07 Nov 2005 15:12:13 +0100] rev 18105
Initial commit of the theory "Weakening".
urbanc [Mon, 07 Nov 2005 14:35:25 +0100] rev 18104
added thms perm, distinct and fresh to the simplifier.
One would liket to add also inject, but this causes
problems with "congruences" like
Lam [a].t1 = Lam [b].t2
P (Lam [a].t1)
-----------------------
P (Lam [b].t2)
because the equation "Lam [a].t1 = Lam [b].t2" would simplify
to "[a].t1 = [b].t2" and then the goal is not true just by
simplification.
haftmann [Mon, 07 Nov 2005 12:06:11 +0100] rev 18103
added proper fillin_mixfix
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