Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.
|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|
|User & Date:||andy 2015-04-15 11:44:40|
|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 to report/arend-report.tex.