equal
deleted
inserted
replaced
15 val advisory_simp : bool Config.T |
15 val advisory_simp : bool Config.T |
16 val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm -> |
16 val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm -> |
17 thm list * thm Seq.seq |
17 thm list * thm Seq.seq |
18 val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic |
18 val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic |
19 val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list -> |
19 val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list -> |
20 thm -> thm Seq.seq |
20 tactic |
21 val metis_lam_transs : string list |
21 val metis_lam_transs : string list |
22 val parse_metis_options : (string list option * string option) parser |
22 val parse_metis_options : (string list option * string option) parser |
23 end |
23 end |
24 |
24 |
25 structure Metis_Tactic : METIS_TACTIC = |
25 structure Metis_Tactic : METIS_TACTIC = |