Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robustness
  2. added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
  3. make workaround possible for Quickcheck with nesting
Changeset 63732:622b54bbe8d4 by blanchet:
more robustness
The file was modified src/HOL/Tools/BNF/bnf_lfp_compat.ML (diff)
Changeset 63731:9f906a2eb0e7 by blanchet:
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
The file was addedsrc/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy
The file was addedsrc/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy
The file was modified src/HOL/ROOT (diff)
Changeset 63730:75f7a77e53bb by blanchet:
make workaround possible for Quickcheck with nesting
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)