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
|