paulson [Tue, 10 Feb 2009 09:46:11 +0000] rev 29852
Deleted the induction rule nat_induct2, which was too weak and not used even once.
nipkow [Mon, 09 Feb 2009 22:15:37 +0100] rev 29851
merged
nipkow [Mon, 09 Feb 2009 22:14:33 +0100] rev 29850
fix to [arith]
nipkow [Mon, 09 Feb 2009 18:50:10 +0100] rev 29849
new attribute "arith" for facts supplied to arith.
Timothy Bourke [Mon, 09 Feb 2009 17:25:07 +1100] rev 29848
Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:
NameSpace.get_accesses has been patched to fix the following
bug:
theory OverHOL imports Main begin
lemma conjI: "a & b --> b"
by blast
ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
val x1 = NameSpace.get_accesses ns "HOL.conjI";
val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
end
where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
but x1 should be just ["HOL.conjI"].
NameSpace.get_accesses is only used within the NameSpace
structure itself. The two uses have been modified to retain
their original behaviour.
Note that NameSpace.valid_accesses gives different results:
get_accesses ns "HOL.eq_class.eq"
gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
but,
valid_accesses ns "HOL.eq_class.eq"
gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]
* Patch FindTheorems:
Prefer names that are shorter to type in the current context.
* Re-export space_of.
chaieb [Mon, 09 Feb 2009 17:21:46 +0000] rev 29847
added Determinants to Library