Thu, 11 Jun 2009 22:04:23 +0200 | bulwahn | masking proof with a quick-and-dirty step | 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 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 |
Tue, 09 Jun 2009 12:05:22 +0200 | bulwahn | refactoring the predicate compiler | file | diff | annotate |
Wed, 20 May 2009 22:24:07 +0200 | haftmann | experimental values command | file | diff | annotate |
Mon, 18 May 2009 15:45:42 +0200 | haftmann | added example on ML level | file | diff | annotate |
Tue, 12 May 2009 21:17:47 +0200 | haftmann | split Predicate_Compile examples into separate theory | file | diff | annotate | base |