equal
deleted
inserted
replaced
12 val non_tautological_facts_of : |
12 val non_tautological_facts_of : |
13 theory -> (((unit -> string) * stature) * thm) list |
13 theory -> (((unit -> string) * stature) * thm) list |
14 val theory_ord : theory * theory -> order |
14 val theory_ord : theory * theory -> order |
15 val thm_ord : thm * thm -> order |
15 val thm_ord : thm * thm -> order |
16 val dependencies_of : string list -> thm -> string list |
16 val dependencies_of : string list -> thm -> string list |
|
17 val goal_of_thm : thm -> thm |
17 val meng_paulson_facts : |
18 val meng_paulson_facts : |
18 Proof.context -> string -> int -> real * real -> thm -> int |
19 Proof.context -> string -> int -> real * real -> thm -> int |
19 -> (((unit -> string) * stature) * thm) list |
20 -> (((unit -> string) * stature) * thm) list |
20 -> ((string * stature) * thm) list |
21 -> ((string * stature) * thm) list |
21 val generate_mash_accessibility : theory -> bool -> string -> unit |
22 val generate_mash_accessibility : theory -> bool -> string -> unit |