src/HOL/ex/Tarski.thy
2012-10-10 wenzelm 2012-10-10 added some ad-hoc namespace prefixes to avoid duplicate facts;
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-03 wenzelm 2010-12-03 recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
2009-06-22 nipkow 2009-06-22 tuned FuncSet
2009-03-02 nipkow 2009-03-02 name changes
2008-12-15 ballarin 2008-12-15 More porting to new locales.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2007-03-29 paulson 2007-03-29 simplified some steps
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 fixed locale fact references;
2006-05-27 wenzelm 2006-05-27 tuned;
2006-03-22 paulson 2006-03-22 Slight simplification of proofs
2006-01-23 paulson 2006-01-23 fixed the <<= notation
2006-01-19 paulson 2006-01-19 strengthened some lemmas; simplified some proofs
2005-10-12 paulson 2005-10-12 tidying
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-15 nipkow 2004-04-15 Added ex/Exceptions.thy
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-07-16 wenzelm 2002-07-16 adapted locales;
2002-05-08 paulson 2002-05-08 Tidied and converted to Isar by lcp
2001-12-10 wenzelm 2001-12-10 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
1999-07-27 wenzelm 1999-07-27 back again, supposedly with correct perms;
1999-07-27 wenzelm 1999-07-27 fixed perms and final nl;
1999-07-26 paulson 1999-07-26 HOL/ex/Tarski: new example by Florian Kammueller