equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 (** theory context references **) |
35 (** theory context references **) |
36 |
36 |
37 val type_definitionN = "Typedef.type_definition"; |
37 val type_definitionN = "Typedef.type_definition"; |
38 val type_definition_def = thm "type_definition_def"; |
38 |
39 |
39 val Rep = thm "type_definition.Rep"; |
40 val Rep = thm "Rep"; |
40 val Rep_inverse = thm "type_definition.Rep_inverse"; |
41 val Rep_inverse = thm "Rep_inverse"; |
41 val Abs_inverse = thm "type_definition.Abs_inverse"; |
42 val Abs_inverse = thm "Abs_inverse"; |
42 val Rep_inject = thm "type_definition.Rep_inject"; |
43 val Rep_inject = thm "Rep_inject"; |
43 val Abs_inject = thm "type_definition.Abs_inject"; |
44 val Abs_inject = thm "Abs_inject"; |
44 val Rep_cases = thm "type_definition.Rep_cases"; |
45 val Rep_cases = thm "Rep_cases"; |
45 val Abs_cases = thm "type_definition.Abs_cases"; |
46 val Abs_cases = thm "Abs_cases"; |
46 val Rep_induct = thm "type_definition.Rep_induct"; |
47 val Rep_induct = thm "Rep_induct"; |
47 val Abs_induct = thm "type_definition.Abs_induct"; |
48 val Abs_induct = thm "Abs_induct"; |
|
49 |
48 |
50 |
49 |
51 |
50 |
52 (** type declarations **) |
51 (** type declarations **) |
53 |
52 |