equal
deleted
inserted
replaced
8 |
8 |
9 signature TACTIC = |
9 signature TACTIC = |
10 sig |
10 sig |
11 val ares_tac : thm list -> int -> tactic |
11 val ares_tac : thm list -> int -> tactic |
12 val asm_rewrite_goal_tac: |
12 val asm_rewrite_goal_tac: |
13 bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
13 bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
14 val assume_tac : int -> tactic |
14 val assume_tac : int -> tactic |
15 val atac : int ->tactic |
15 val atac : int ->tactic |
16 val bimatch_from_nets_tac: |
16 val bimatch_from_nets_tac: |
17 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
17 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
18 val bimatch_tac : (bool*thm)list -> int -> tactic |
18 val bimatch_tac : (bool*thm)list -> int -> tactic |