equal
deleted
inserted
replaced
95 val simple_fact: 'a -> ('a * 'b list) list |
95 val simple_fact: 'a -> ('a * 'b list) list |
96 val tag_rule: string * string -> thm -> thm |
96 val tag_rule: string * string -> thm -> thm |
97 val untag_rule: string -> thm -> thm |
97 val untag_rule: string -> thm -> thm |
98 val tag: string * string -> attribute |
98 val tag: string * string -> attribute |
99 val untag: string -> attribute |
99 val untag: string -> attribute |
|
100 val is_free_dummy: thm -> bool |
|
101 val tag_free_dummy: thm -> thm |
100 val def_name: string -> string |
102 val def_name: string -> string |
101 val def_name_optional: string -> string -> string |
103 val def_name_optional: string -> string -> string |
102 val def_binding: Binding.binding -> Binding.binding |
104 val def_binding: Binding.binding -> Binding.binding |
103 val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding |
105 val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding |
104 val has_name_hint: thm -> bool |
106 val has_name_hint: thm -> bool |
582 |
584 |
583 fun tag tg = rule_attribute (K (tag_rule tg)); |
585 fun tag tg = rule_attribute (K (tag_rule tg)); |
584 fun untag s = rule_attribute (K (untag_rule s)); |
586 fun untag s = rule_attribute (K (untag_rule s)); |
585 |
587 |
586 |
588 |
|
589 (* free dummy thm -- for abstract closure *) |
|
590 |
|
591 val free_dummyN = "free_dummy"; |
|
592 fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; |
|
593 val tag_free_dummy = tag_rule (free_dummyN, ""); |
|
594 |
|
595 |
587 (* def_name *) |
596 (* def_name *) |
588 |
597 |
589 fun def_name c = c ^ "_def"; |
598 fun def_name c = c ^ "_def"; |
590 |
599 |
591 fun def_name_optional c "" = def_name c |
600 fun def_name_optional c "" = def_name c |