equal
deleted
inserted
replaced
678 (* outer syntax *) |
678 (* outer syntax *) |
679 |
679 |
680 val _ = |
680 val _ = |
681 Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} |
681 Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} |
682 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" |
682 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" |
683 (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name -- |
683 (Parse.name -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name -- |
684 (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) => |
684 (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) => |
685 prove_strong_ind name avoids)); |
685 prove_strong_ind name avoids)); |
686 |
686 |
687 val _ = |
687 val _ = |
688 Outer_Syntax.local_theory @{command_keyword equivariance} |
688 Outer_Syntax.local_theory @{command_keyword equivariance} |
689 "prove equivariance for inductive predicate involving nominal datatypes" |
689 "prove equivariance for inductive predicate involving nominal datatypes" |
690 (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >> |
690 (Parse.name -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >> |
691 (fn (name, atoms) => prove_eqvt name atoms)); |
691 (fn (name, atoms) => prove_eqvt name atoms)); |
692 |
692 |
693 end |
693 end |