Theory SpecCheck_Dynamic

✐‹creator "Kevin Kappelmann"›
section ‹Dynamic Generators›
theory SpecCheck_Dynamic
imports SpecCheck
begin

paragraph ‹Summary›
text ‹Generators and show functions for SpecCheck that are dynamically derived from a given ML input
string. This approach can be handy to quickly test a function during development, but it lacks
customisability and is very brittle. See @{file "../Examples/SpecCheck_Examples.thy"} for some
examples contrasting this approach to the standard one (specifying generators as ML code).›

ML_file ‹dynamic_construct.ML›
ML_file ‹speccheck_dynamic.ML›

end