src/HOL/MetisExamples/Abstraction.thy
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-05-07 berghofe 2008-05-07 Replaced union_empty2 by Un_empty_right.
2007-10-04 paulson 2007-10-04 combinator translation
2007-09-30 wenzelm 2007-09-30 avoid internal names;
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-07-11 berghofe 2007-07-11 Adapted to changes in Predicate theory.
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-21 paulson 2007-06-21 integration of Metis prover