on bbefa33 help sign in
all commits
a0d8376Merge pull request #2518 from jeremy-w/jeremy-w/mark-interactive-proving-as-deprecatedNiklas Larsson 7f6f3c4Spelling in Sphinx documentationEcho Nolan 90b7d07Point readers at Elaborator ReflectionJeremy W. Sherman 156fb5aDocument interactive theorem proving as deprecated.Jeremy W. Sherman 696f336Replace "metavariable" with "hole"Michael Gilliland 87039fbHeading normalisation, and reST usage fixes.Jan de Muijnck-Hughes 029413bTypo fixEdwin Brady 035f24eMove tactic proofs out of main tutorialEdwin Brady