src/HOL/ex/Predicate_Compile_ex.thy
Thu, 11 Jun 2009 22:04:23 +0200 bulwahn masking proof with a quick-and-dirty step
Thu, 11 Jun 2009 21:37:26 +0200 bulwahn improved infrastructure of predicate compiler for adding manual introduction rules
Thu, 11 Jun 2009 12:06:13 +0200 bulwahn making isatest happy; but misunderstanding remains
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
Tue, 09 Jun 2009 12:05:22 +0200 bulwahn refactoring the predicate compiler
Wed, 20 May 2009 22:24:07 +0200 haftmann experimental values command
Mon, 18 May 2009 15:45:42 +0200 haftmann added example on ML level
Tue, 12 May 2009 21:17:47 +0200 haftmann split Predicate_Compile examples into separate theory
less more (0) tip