Check-in [caa7fbdd73]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added screen shot of the proof assistant, starting a proof.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:caa7fbdd73265ada6bb170a4871b156b529268ce
User & Date: andy 2015-04-15 11:44:40
Context
2015-04-15
11:47
Split the `What` argument to elaborate into `What` and `Data`. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk
11:44
Added screen shot of the proof assistant, starting a proof. check-in: caa7fbdd73 user: andy tags: trunk
11:12
Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.) check-in: e902cf4ec5 user: andy tags: trunk
Changes
Unified Diffs Side-by-Side Diffs Patch

Changes to report/arend-report.tex.

Added report/proof-start-sample.png.