[isabelle-dev] NEWS: HOL-Spec_Check -- a Quickcheck tool for Isabelle's ML environment

Lukas Bulwahn bulwahn at in.tum.de
Fri May 31 07:36:40 CEST 2013

Previous message (by thread): [isabelle-dev] Mira / AFP configuration problem?
Next message (by thread): [isabelle-dev] Error with case syntax?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.

   With HOL-Spec_Check, ML developers can check specifications with the
   ML function check_property. The specifications must be of the form
   "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
   src/HOL/Spec_Check/Examples.thy.

Lukas

Previous message (by thread): [isabelle-dev] Mira / AFP configuration problem?
Next message (by thread): [isabelle-dev] Error with case syntax?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list