--- a/src/HOL/Spec_Check/README Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-This is a Quickcheck tool for Isabelle's ML environment.
-
-Authors
-
- Lukas Bulwahn
- Nicolai Schaffroth
-
-Quick Usage
-
- - Import Spec_Check.thy in your development
- - Look at examples in Examples.thy
- - write specifications with the ML invocation
- check_property "ALL x. P x"
-
-Notes
-
-Our specification-based testing tool originated from Christopher League's
-QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
-provides a rich and uniform ML platform (called Isabelle/ML), this
-testing tools is very different than the one for a typical ML developer.
-
-1. Isabelle/ML provides common data structures, which we can use in the
-tool's implementation for storing data and printing output.
-
-2. The implementation in Isabelle that will be checked with this tool
-commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
-but they do not use other integer types in ML, such as ML's Int.int,
-Word.word and others.
-
-3. As Isabelle can run heavily in parallel, we avoid reference types.
-
-4. Isabelle has special naming conventions and documentation of source
-code is only minimal to avoid parroting.
-
-Next steps:
- - Remove all references and store the neccessary random seed in the
- Isabelle's context.
- - Simplify some existing random generators.
- The original ones from Christopher League are so complicated to
- support many integer types uniformly.
-
-License
-
- The source code originated from Christopher League's QCheck, which is
- licensed under the 2-clause BSD license. The current source code is
- licensed under the compatible 3-clause BSD license of Isabelle.
-