src/HOL/Prolog/prolog.ML
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-30 wenzelm 2009-07-30 FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
2009-07-28 wenzelm 2009-07-28 eliminated METAHYPS;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 ptac/prolog_tac: proper context;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2006-11-20 wenzelm 2006-11-20 HOL-Prolog: converted legacy ML scripts;