Check-in [95a716e7e5]

Not logged in

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

Overview
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
SHA1:95a716e7e5720454efda602616362f2c32281dad
User & Date: andy 2015-04-18 16:44:05
Context
2015-04-18
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
2015-04-16
22:02
Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk
Changes
Unified Diffs Side-by-Side Diffs Patch

Changes to plsrc/nat_spec_demo.pl.