equal
deleted
inserted
replaced
773 |
773 |
774 val setup = |
774 val setup = |
775 add_codegen "inductive" inductive_codegen #> |
775 add_codegen "inductive" inductive_codegen #> |
776 Attrib.setup @{binding code_ind} |
776 Attrib.setup @{binding code_ind} |
777 (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- |
777 (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- |
778 Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add)) |
778 Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add)) |
779 "introduction rules for executable predicates"; |
779 "introduction rules for executable predicates"; |
780 |
780 |
781 (**** Quickcheck involving inductive predicates ****) |
781 (**** Quickcheck involving inductive predicates ****) |
782 |
782 |
783 val test_fn : (int * int * int -> term list option) Unsynchronized.ref = |
783 val test_fn : (int * int * int -> term list option) Unsynchronized.ref = |