Hi all,
Let's consider any theorem that depends on the BOOL_CASES_AX. For example,
from the HOL Reference:
> [AND_CLAUSES] Theorem
>
> [oracles: ] [axioms: BOOL_CASES_AX] []
> |- !t.
> (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
> (t /\ F <=> F) /\ (t /\ t <=> t)
But if now I display in my HOL system the theorem, with the option
"show_tags := true", this is what I get:
> val it =
> [oracles: DISK_THM] [axioms: ] []
> |- ∀t.
> (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔
t)
How comes the axiom is not displayed, and there is a "DISK_THM" oracle
instead?
Thank you,
Andrea
------------------------------------------------------------------------------
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
