Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.
|Comment:||Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate.|
|Downloads:||Tarball | ZIP archive | SQL archive|
|Timelines:||family | ancestors | descendants | both | trunk|
|Files:||files | file ages | folders|
|User & Date:||andy 2015-04-18 16:44:05|
|16:44||Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk|
|16:44||Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk|
|22:02||Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk|
Changes to plsrc/nat_spec_demo.pl.