src/HOL/Import/HOL4Compat.thy
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-11-18 haftmann 2010-11-18 map_pair replaces prod_fun
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-03-23 haftmann 2009-03-23 more canonical import, syntax fix
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2008-12-10 wenzelm 2008-12-10 fixed import: requires ContNotDenum;
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-31 krauss 2006-07-31 Removed an "apply arith" where there are already "No Subgoals"
2006-02-15 obua 2006-02-15 fixed bugs, added caching
2005-08-29 obua 2005-08-29 Updated import.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-04-17 skalberg 2004-04-17 Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.