src/HOL/Import/HOLLightReal.thy
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-01 Cezary Kaliszyk 2011-09-01 HOL/Import: observe distinction between sets and predicates (where possible)
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-07-13 Cezary Kaliszyk 2011-07-13 HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems