equal
deleted
inserted
replaced
21 val selections: string * thm list -> (ref * thm) list |
21 val selections: string * thm list -> (ref * thm) list |
22 type T |
22 type T |
23 val empty: T |
23 val empty: T |
24 val intern: T -> xstring -> string |
24 val intern: T -> xstring -> string |
25 val extern: T -> string -> xstring |
25 val extern: T -> string -> xstring |
26 val lookup: Context.generic -> T -> string -> thm list option |
26 val lookup: Context.generic -> T -> string -> (bool * thm list) option |
27 val defined: T -> string -> bool |
27 val defined: T -> string -> bool |
28 val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a |
28 val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a |
29 val dest_static: T list -> T -> (string * thm list) list |
29 val dest_static: T list -> T -> (string * thm list) list |
30 val extern_static: T list -> T -> (xstring * thm list) list |
30 val extern_static: T list -> T -> (xstring * thm list) list |
31 val props: T -> thm list |
31 val props: T -> thm list |
142 val defined = Symtab.defined o table_of; |
142 val defined = Symtab.defined o table_of; |
143 |
143 |
144 fun lookup context facts name = |
144 fun lookup context facts name = |
145 (case Symtab.lookup (table_of facts) name of |
145 (case Symtab.lookup (table_of facts) name of |
146 NONE => NONE |
146 NONE => NONE |
147 | SOME (Static ths, _) => SOME ths |
147 | SOME (Static ths, _) => SOME (true, ths) |
148 | SOME (Dynamic f, _) => SOME (f context)); |
148 | SOME (Dynamic f, _) => SOME (false, f context)); |
149 |
149 |
150 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of; |
150 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of; |
151 |
151 |
152 |
152 |
153 (* content difference *) |
153 (* content difference *) |