on b0cb4e2 help sign in
all commits
9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman f8759cdIDESlave support for setting the depth of interactive proof searchDavid Raymond Christiansen 094be98Add an optional depth to 'search' tacticEdwin Brady 659e985Add IDESlave support to :makelemmaDavid Raymond Christiansen a265279:makelemma now works on provisional definitionsEdwin Brady 719d472'search' now fails if there are metavariablesEdwin Brady 50f63b5Make sensible implicit choices in :addlemmaEdwin Brady f8e6549:addclause now adds template bodies to instancesEdwin Brady db88c3eTidy output of :makelemmaEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady dae7d7dMove interactive commands to their own moduleEdwin Brady