wenzelm [Fri, 21 Sep 2007 22:51:08 +0200] rev 24669
proper signature constraint;
minor tuning;
wenzelm [Thu, 20 Sep 2007 20:58:40 +0200] rev 24668
added interrupt_timeout;
tuned signature;
wenzelm [Thu, 20 Sep 2007 20:56:54 +0200] rev 24667
Generic interpretation of theory data.
wenzelm [Thu, 20 Sep 2007 20:56:34 +0200] rev 24666
tuned signature;
moved generic interpretation to interpretation.ML;
added abstract at_begin/end wrappers;
wenzelm [Thu, 20 Sep 2007 20:56:33 +0200] rev 24665
avoid Theory.rep_theory;
wenzelm [Thu, 20 Sep 2007 20:56:32 +0200] rev 24664
added interpretation.ML;
wenzelm [Thu, 20 Sep 2007 17:48:16 +0200] rev 24663
improved error behaviour of use (bootstrap version);
haftmann [Thu, 20 Sep 2007 16:37:34 +0200] rev 24662
more precise treatment of free dictionary parameters for evaluation
haftmann [Thu, 20 Sep 2007 16:37:33 +0200] rev 24661
fixed cg setup
haftmann [Thu, 20 Sep 2007 16:37:32 +0200] rev 24660
restored ml system independence
haftmann [Thu, 20 Sep 2007 16:37:31 +0200] rev 24659
more permissive
haftmann [Thu, 20 Sep 2007 16:37:30 +0200] rev 24658
clarified code lemmas
haftmann [Thu, 20 Sep 2007 16:37:29 +0200] rev 24657
fixed wrong syntax treatment in class target
haftmann [Thu, 20 Sep 2007 16:37:28 +0200] rev 24656
code lemmas for cardinality
berghofe [Thu, 20 Sep 2007 16:23:12 +0200] rev 24655
- eval_term no longer computes result during compile time
- generated ML code is now compiled via ML_Context.use_mltext
rather than use_text; this makes sure that antiquotations
are expanded
- quickcheck now checks whether types to be substituted for
type variables have correct sorts; this avoids spurious
counterexamples
- execution time for auto_quickcheck is now limited