# Theory Synthetic_Definition

section‹Automatic synthesis of formulas›
theory Synthetic_Definition
imports
Utils
keywords
"synthesize" :: thy_decl % "ML"
and
"synthesize_notc" :: thy_decl % "ML"
and
"generate_schematic" :: thy_decl % "ML"
and
"arity_theorem" :: thy_decl % "ML"
and
"manual_schematic" :: thy_goal_stmt % "ML"
and
"manual_arity" :: thy_goal_stmt % "ML"
and
"from_schematic"
and
"for"
and
"from_definition"
and
"assuming"
and
"intermediate"
begin
named_theorems fm_definitions "Definitions of synthetized formulas."
named_theorems iff_sats "Theorems for synthetising formulas."
named_theorems arity "Theorems for arity of formulas."
named_theorems arity_aux "Auxiliary theorems for calculating arities."
ML_file‹Synthetic_Definition.ml›
text‹The \<^ML>‹synthetic_def› function extracts definitions from
schematic goals. A new definition is added to the context. ›
end