src/HOL/UNITY/Transformers.thy
2012-03-13 wenzelm 2012-03-13 tuned proofs;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-09 haftmann 2011-08-09 tuned proofs
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-09-16 haftmann 2009-09-16 Inter and Union are mere abbreviations for Inf and Sup
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 ^^
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-08-20 haftmann 2007-08-20 Sup now explicit parameter of complete_lattice
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-12-10 nipkow 2006-12-10 Modified lattice locale
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-10-13 berghofe 2006-10-13 Adapted to changes in FixedPoint theory.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2003-03-21 paulson 2003-03-21 More on progress sets
2003-03-17 paulson 2003-03-17 More "progress set" material
2003-03-14 paulson 2003-03-14 Proved the main lemma on progress sets
2003-03-10 paulson 2003-03-10 New theory ProgressSets. Definition of closure sets
2003-03-06 paulson 2003-03-06 new UNITY examples theory
2003-02-26 paulson 2003-02-26 completed proofs for programs consisting of a single assignment
2003-02-18 paulson 2003-02-18 new theory Transformers: Meier-Sanders non-interference theory