equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature GLOBAL_THEORY = |
7 signature GLOBAL_THEORY = |
8 sig |
8 sig |
9 val facts_of: theory -> Facts.T |
9 val facts_of: theory -> Facts.T |
|
10 val fact_space: theory -> Name_Space.T |
10 val check_fact: theory -> xstring * Position.T -> string |
11 val check_fact: theory -> xstring * Position.T -> string |
11 val intern_fact: theory -> xstring -> string |
12 val intern_fact: theory -> xstring -> string |
12 val defined_fact: theory -> string -> bool |
13 val defined_fact: theory -> string -> bool |
13 val alias_fact: binding -> string -> theory -> theory |
14 val alias_fact: binding -> string -> theory -> theory |
14 val hide_fact: bool -> string -> theory -> theory |
15 val hide_fact: bool -> string -> theory -> theory |
71 (* facts *) |
72 (* facts *) |
72 |
73 |
73 val facts_of = #1 o Data.get; |
74 val facts_of = #1 o Data.get; |
74 val map_facts = Data.map o apfst; |
75 val map_facts = Data.map o apfst; |
75 |
76 |
|
77 val fact_space = Facts.space_of o facts_of; |
76 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy); |
78 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy); |
77 val intern_fact = Facts.intern o facts_of; |
79 val intern_fact = Facts.intern o facts_of; |
78 val defined_fact = Facts.defined o facts_of; |
80 val defined_fact = Facts.defined o facts_of; |
79 |
81 |
80 fun alias_fact binding name thy = |
82 fun alias_fact binding name thy = |