Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Predicate_Compile_Quickcheck.thy
author wenzelm
Sat, 14 May 2011 12:40:11 +0200
changeset 42800 df2dc9406287
parent 39252 8f176e575a49
child 43886 bf068e758783
permissions -rw-r--r--
just one universal Proof.context -- discontinued claset/clasimpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset 
     1
 
(* Author: Lukas Bulwahn, TU Muenchen *)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset 
     2
 












0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     3


header {* A Prototype of Quickcheck based on the Predicate Compiler *}













0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     4














0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     5


theory Predicate_Compile_Quickcheck













0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     6


imports Main Predicate_Compile_Alternative_Defs













0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     7


uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"













0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     8


begin













0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




     9









39252






8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    10


setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term













8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    11


  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}













8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    12


setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",













8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    13


  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}













8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    14


setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",













8f176e575a49
changing the container for the quickcheck options to a generic data



bulwahn


parents: 
36026

diff
changeset




    15


  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}








35953






0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




    16














0460ff79bb52
moved further predicate compile files to HOL-Library



bulwahn


parents: 

diff
changeset




    17


end














isabelle