equal
deleted
inserted
replaced
30 structure CaseSplitData_HOL : CASE_SPLIT_DATA = |
30 structure CaseSplitData_HOL : CASE_SPLIT_DATA = |
31 struct |
31 struct |
32 val dest_Trueprop = HOLogic.dest_Trueprop; |
32 val dest_Trueprop = HOLogic.dest_Trueprop; |
33 val mk_Trueprop = HOLogic.mk_Trueprop; |
33 val mk_Trueprop = HOLogic.mk_Trueprop; |
34 |
34 |
35 val atomize = thms "induct_atomize"; |
35 val atomize = @{thms induct_atomize}; |
36 val rulify = thms "induct_rulify"; |
36 val rulify = @{thms induct_rulify}; |
37 val rulify_fallback = thms "induct_rulify_fallback"; |
37 val rulify_fallback = @{thms induct_rulify_fallback}; |
38 |
38 |
39 end; |
39 end; |
40 |
40 |
41 |
41 |
42 signature CASE_SPLIT = |
42 signature CASE_SPLIT = |