[Logiweb] Referencing faulty pages

[Frederik Eriksen]

Hi logiweb at diku.dk

Suppose you're working on a page called B, which references a page 
called A. Page A is faulty; that is, it wasn't deemed correct by the 
proof checker. In contrast, page B in itself is not faulty. Now you let 
the proof checker verify page B. What happens? Will the checker take the 
correctness of page A for granted, or will it deem page B faulty because 
it references faulty lemmas from page A?

Best Regards
Frederik Eriksen.