1signature extra_pred_setTools = 2sig 3 4 (* Simple *) 5 val pset_set_ss : simpLib.simpset 6 val pset_elt_ss : simpLib.simpset 7 8 val pset_ss : simpLib.simpset 9 val PSET_TAC : Thm.thm list -> Abbrev.tactic 10 11end
1signature extra_pred_setTools = 2sig 3 4 (* Simple *) 5 val pset_set_ss : simpLib.simpset 6 val pset_elt_ss : simpLib.simpset 7 8 val pset_ss : simpLib.simpset 9 val PSET_TAC : Thm.thm list -> Abbrev.tactic 10 11end