equal
deleted
inserted
replaced
11 val freeze : term -> term |
11 val freeze : term -> term |
12 val mutate_exc : term -> string list -> int -> term list |
12 val mutate_exc : term -> string list -> int -> term list |
13 val mutate_sign : term -> theory -> (string * string) list -> int -> term list |
13 val mutate_sign : term -> theory -> (string * string) list -> int -> term list |
14 val mutate_mix : term -> theory -> string list -> |
14 val mutate_mix : term -> theory -> string list -> |
15 (string * string) list -> int -> term list |
15 (string * string) list -> int -> term list |
16 |
|
17 val all_unconcealed_thms_of : theory -> (string * thm) list |
|
18 end; |
16 end; |
19 |
17 |
20 structure Mutabelle : MUTABELLE = |
18 structure Mutabelle : MUTABELLE = |
21 struct |
19 struct |
22 |
|
23 fun all_unconcealed_thms_of thy = |
|
24 let |
|
25 val facts = Global_Theory.facts_of thy |
|
26 in |
|
27 Facts.fold_static |
|
28 (fn (s, ths) => |
|
29 if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths)) |
|
30 facts [] |
|
31 end; |
|
32 |
20 |
33 fun consts_of thy = |
21 fun consts_of thy = |
34 let |
22 let |
35 val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy) |
23 val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy) |
36 in |
24 in |