equal
deleted
inserted
replaced
418 setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del) |
418 setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del) |
419 "declaration of definitional transformations" #> |
419 "declaration of definitional transformations" #> |
420 setup (Binding.name "abs_def") |
420 setup (Binding.name "abs_def") |
421 (Scan.succeed (Thm.rule_attribute (fn context => |
421 (Scan.succeed (Thm.rule_attribute (fn context => |
422 Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))) |
422 Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))) |
423 "abstract over free variables of definitionial theorem")); |
423 "abstract over free variables of definitional theorem")); |
424 |
424 |
425 |
425 |
426 |
426 |
427 (** configuration options **) |
427 (** configuration options **) |
428 |
428 |