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
Wed, 01 Sep 2010 18:18:47 +0200
changeset 38976 a4a465dc89d9
parent 36026 276ebec72082
child 39252 8f176e575a49
permissions -rw-r--r--
Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;
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









36026






276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

diff
changeset




    10


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













276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

diff
changeset




    11


  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}













276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

diff
changeset




    12


setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",













276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

diff
changeset




    13


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













276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

diff
changeset




    14


setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",













276ebec72082
adopting Predicate_Compile_Quickcheck



bulwahn


parents: 
35953

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