equal
deleted
inserted
replaced
1963 if_bool_eq_disj [no_atp] |
1963 if_bool_eq_disj [no_atp] |
1964 |
1964 |
1965 |
1965 |
1966 subsection {* Preprocessing for the predicate compiler *} |
1966 subsection {* Preprocessing for the predicate compiler *} |
1967 |
1967 |
1968 ML {* |
1968 named_theorems code_pred_def |
1969 structure Predicate_Compile_Alternative_Defs = Named_Thms |
1969 "alternative definitions of constants for the Predicate Compiler" |
1970 ( |
1970 named_theorems code_pred_inline |
1971 val name = @{binding code_pred_def} |
1971 "inlining definitions for the Predicate Compiler" |
1972 val description = "alternative definitions of constants for the Predicate Compiler" |
1972 named_theorems code_pred_simp |
1973 ) |
1973 "simplification rules for the optimisations in the Predicate Compiler" |
1974 structure Predicate_Compile_Inline_Defs = Named_Thms |
|
1975 ( |
|
1976 val name = @{binding code_pred_inline} |
|
1977 val description = "inlining definitions for the Predicate Compiler" |
|
1978 ) |
|
1979 structure Predicate_Compile_Simps = Named_Thms |
|
1980 ( |
|
1981 val name = @{binding code_pred_simp} |
|
1982 val description = "simplification rules for the optimisations in the Predicate Compiler" |
|
1983 ) |
|
1984 *} |
|
1985 |
|
1986 setup {* |
|
1987 Predicate_Compile_Alternative_Defs.setup |
|
1988 #> Predicate_Compile_Inline_Defs.setup |
|
1989 #> Predicate_Compile_Simps.setup |
|
1990 *} |
|
1991 |
1974 |
1992 |
1975 |
1993 subsection {* Legacy tactics and ML bindings *} |
1976 subsection {* Legacy tactics and ML bindings *} |
1994 |
1977 |
1995 ML {* |
1978 ML {* |