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.
* means: has received copy.
David Aspinall*
Clemens Ballarin*
Gertrud Bauer*
Stefan Berghofer*
Gerwin Klein*
David von Oheimb*
Farhad Mehta*
Stephan Merz*
Leonor Prensa Nieto*
Cornelia Pusch
Bernhard Rumpe (wants a signed copy!)*
Norbert Schirmer*
Martin Strecker*
Ralf Steinbrueggen*
Essential colleagues:
Prof. Harald Ganzinger*
Max-Planck-Institut für Informatik
Im Stadtwald
66123 Saarbrücken
Prof. Bob Boyer*
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.
Prof. J Moore*
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188
U.S.A.
Prof. Frank Pfenning*
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891
U.S.A.
Dr. Shankar*
SRI International
333 Ravenswood Avenue,
Menlo Park, CA, 94025-3493
U.S.A.
Prof. Andrei Voronkov*
Department of Computer Science
The University of Manchester
Oxford Road
Manchester M13 9PL
England
Cambridge people:
Tony Hoare
Mike Gordon*
Sidi Ehmety
Frederic Blanqui*
James Margetson
Robin Milner*
Sara Kalvala
(for contributing comments)
dr. Stefano Bistarelli*
Istituto per le Applicazioni Telematiche
C.N.R. Pisa
Area della Ricerca, Via G. Moruzzi, 1
56124 Pisa
Italien
Gergely Buday*
Karl-Ferlemann Str. 16.
04177 Leipzig
Tanja Vos*
C/ Ing. Joaquin Benlloch 85-Esc A-25
46026 Valencia
Spain
Further colleagues:
Manfred Broy*
Ursula Martin*
School of Computer Science
University of St Andrews
St Andrews KY16 6SS
Scotland
UK