src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63731 9f906a2eb0e7
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
     1 theory Quickcheck_Nesting
     2 imports Main
     3 begin
     4 
     5 ML \<open>
     6 let
     7   open BNF_FP_Def_Sugar
     8   open BNF_LFP_Compat
     9 
    10   val compat_plugin = Plugin_Name.declare_setup @{binding compat};
    11 
    12   fun compat fp_sugars =
    13     perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));
    14 in
    15   Theory.setup (fp_sugars_interpretation compat_plugin compat)
    16 end
    17 \<close>
    18 
    19 end