| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch changed mode inference of predicate compiler to return infered dataflow
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch generic compilation of predicate compiler with different monads
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:27 +0200 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 15:58:12 +0200 |
bulwahn |
commented trancl example; added debug message
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 14:54:30 +0200 |
bulwahn |
exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:33:58 +0200 |
bulwahn |
added diagnostic printing; changed proof for parameters; moved code
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 18:33:58 +0200 |
bulwahn |
added cases to code_pred command
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:39:08 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:37:26 +0200 |
bulwahn |
improved infrastructure of predicate compiler for adding manual introduction rules
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 14:25:58 +0200 |
wenzelm |
merged, reverting workarounds on both sides;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:48:38 +0200 |
wenzelm |
added sporadic (Local)Theory.checkpoint, to enable parallel proof checking;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:06:13 +0200 |
bulwahn |
making isatest happy; but misunderstanding remains
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 21:04:36 +0200 |
bulwahn |
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 10:42:24 +0200 |
bulwahn |
tuned; corrected exception handling
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 00:46:37 +0200 |
wenzelm |
simplified Graph.extend;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 19:41:27 +0200 |
bulwahn |
avoiding duplicate definitions of executable functions
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 14:20:37 +0200 |
bulwahn |
removed general graph functions in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 13:40:57 +0200 |
bulwahn |
removed debug messages
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 12:05:22 +0200 |
bulwahn |
refactoring the predicate compiler
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:00:44 +0200 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
| Sun, 31 May 2009 17:45:53 +0200 |
wenzelm |
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
|
file |
diff |
annotate
|
| Thu, 28 May 2009 20:01:38 +0200 |
bulwahn |
added remark to code
|
file |
diff |
annotate
|
| Wed, 20 May 2009 22:24:07 +0200 |
haftmann |
experimental values command
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:17:59 +0200 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file |
diff |
annotate
|
| Fri, 15 May 2009 15:56:28 +0200 |
bulwahn |
added predicate transformation function for code generation
|
file |
diff |
annotate
|
| Fri, 15 May 2009 15:29:34 +0200 |
bulwahn |
added predicate transformation function for code generation
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:09:36 +0200 |
haftmann |
marginally tuned
|
file |
diff |
annotate
|
| Mon, 11 May 2009 20:09:03 +0200 |
haftmann |
fixed merge accident
|
file |
diff |
annotate
|
| Mon, 11 May 2009 17:20:52 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:39:53 +0200 |
bulwahn |
fixed code_pred command
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:18:42 +0200 |
bulwahn |
Added pred_code command
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 11:10:23 +0200 |
bulwahn |
added general preprocessing of equality in predicates for code generation
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 17:45:16 +0200 |
haftmann |
some experiements towards user interface for predicate compiler
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 14:43:51 +0100 |
haftmann |
NameSpace.base_name ~> Long_Name.base_name
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 09:37:33 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:25:28 +0100 |
haftmann |
added predicate compiler, as formally checked prototype, not as user package
|
file |
diff |
annotate
|