304 setup (Binding.name "elim_format") (Scan.succeed elim_format) |
304 setup (Binding.name "elim_format") (Scan.succeed elim_format) |
305 "destruct rule turned into elimination rule format" #> |
305 "destruct rule turned into elimination rule format" #> |
306 setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #> |
306 setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #> |
307 setup (Binding.name "eta_long") (Scan.succeed eta_long) |
307 setup (Binding.name "eta_long") (Scan.succeed eta_long) |
308 "put theorem into eta long beta normal form" #> |
308 "put theorem into eta long beta normal form" #> |
309 setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize) |
309 setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize) |
310 "declaration of atomize rule" #> |
310 "declaration of atomize rule" #> |
311 setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify) |
311 setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify) |
312 "declaration of rulify rule" #> |
312 "declaration of rulify rule" #> |
313 setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #> |
313 setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #> |
314 setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del) |
314 setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del) |
315 "declaration of definitional transformations" #> |
315 "declaration of definitional transformations" #> |
316 setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def))) |
316 setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def))) |