on 9f65713 help sign in
all commits
8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady 07f12f9Separate elaboration of declarations and termsEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 1b1a055Improved where; implicit arguments now expanded during elaborationEdwin Brady f7a7f0bSome proofs in nat.idrEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady