haftmann [Thu, 26 Apr 2007 13:33:07 +0200] rev 22802
replaced recdef by function
haftmann [Thu, 26 Apr 2007 13:33:05 +0200] rev 22801
cleaned up code generator setup for int
haftmann [Thu, 26 Apr 2007 13:33:04 +0200] rev 22800
added lemmatas
haftmann [Thu, 26 Apr 2007 13:32:59 +0200] rev 22799
moved code generation pretty integers and characters to separate theories
haftmann [Thu, 26 Apr 2007 13:32:55 +0200] rev 22798
updated doc
wenzelm [Thu, 26 Apr 2007 12:00:12 +0200] rev 22797
mk_const_def: Sign.intern_term (legacy);
wenzelm [Thu, 26 Apr 2007 12:00:05 +0200] rev 22796
renamed some old names Theory.xxx to Sign.xxx;
wenzelm [Thu, 26 Apr 2007 12:00:01 +0200] rev 22795
updated;
narboux [Wed, 25 Apr 2007 21:29:14 +0200] rev 22794
add the lemma supp_eqvt and put the right attribute
nipkow [Wed, 25 Apr 2007 17:50:48 +0200] rev 22793
new lemma splice_length
narboux [Wed, 25 Apr 2007 15:38:56 +0200] rev 22792
fix sml compilation
berghofe [Wed, 25 Apr 2007 15:26:01 +0200] rev 22791
Moved function params_of to inductive_package.ML.
berghofe [Wed, 25 Apr 2007 15:25:22 +0200] rev 22790
Moved functions infer_intro_vars, arities_of, params_of, and
partition_rules to inductive_package.ML.
berghofe [Wed, 25 Apr 2007 15:24:15 +0200] rev 22789
Added functions arities_of, params_of, partition_rules, and
infer_intro_vars (from inductive_realizer.ML).
berghofe [Wed, 25 Apr 2007 15:22:57 +0200] rev 22788
eqvt_tac now instantiates introduction rules before applying them.
narboux [Tue, 24 Apr 2007 18:06:04 +0200] rev 22787
update fresh_fun_simp for debugging purposes
narboux [Tue, 24 Apr 2007 17:16:55 +0200] rev 22786
fixes last commit
narboux [Tue, 24 Apr 2007 16:44:11 +0200] rev 22785
add two lemmas dealing with freshness on permutations.
berghofe [Tue, 24 Apr 2007 15:19:33 +0200] rev 22784
Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe [Tue, 24 Apr 2007 15:18:42 +0200] rev 22783
Added datatype_case.
berghofe [Tue, 24 Apr 2007 15:18:09 +0200] rev 22782
Added intro / elim rules for prod_case.
berghofe [Tue, 24 Apr 2007 15:17:22 +0200] rev 22781
sum_case is now authentic.
berghofe [Tue, 24 Apr 2007 15:15:52 +0200] rev 22780
Adapted to new parse translation for case expressions.
berghofe [Tue, 24 Apr 2007 15:14:31 +0200] rev 22779
Parse / print translations for nested case expressions, taken
from Konrad Slind's TFL package.
berghofe [Tue, 24 Apr 2007 15:13:19 +0200] rev 22778
Streamlined datatype_codegen function using new datatype_of_case
and datatype_of_constr functions.
berghofe [Tue, 24 Apr 2007 15:11:07 +0200] rev 22777
- Moved parse / print translations for case to datatype_case.ML
- Added new functions datatype_of_constr and datatype_of_case
to retrieve datatype corresponding to name of constructor
or case combinator.
berghofe [Tue, 24 Apr 2007 15:07:27 +0200] rev 22776
case constants are now authentic.
narboux [Tue, 24 Apr 2007 14:02:16 +0200] rev 22775
oups : wrong commit
narboux [Tue, 24 Apr 2007 14:01:23 +0200] rev 22774
adds op in front of an infix to fix SML compilation
wenzelm [Mon, 23 Apr 2007 20:44:12 +0200] rev 22773
sane version of read_termTs (proper freeze);
added read_terms, cert_terms;