equal
deleted
inserted
replaced
13 end |
13 end |
14 |
14 |
15 structure NominalInductive2 : NOMINAL_INDUCTIVE2 = |
15 structure NominalInductive2 : NOMINAL_INDUCTIVE2 = |
16 struct |
16 struct |
17 |
17 |
18 val inductive_forall_def = @{thm induct_forall_def}; |
18 val inductive_forall_def = @{thm HOL.induct_forall_def}; |
19 val inductive_atomize = @{thms induct_atomize}; |
19 val inductive_atomize = @{thms induct_atomize}; |
20 val inductive_rulify = @{thms induct_rulify}; |
20 val inductive_rulify = @{thms induct_rulify}; |
21 |
21 |
22 fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify []; |
22 fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify []; |
23 |
23 |