src/HOL/IMP/Abs_Int3.thy
2015-12-19 haftmann 2015-12-19 abandoned attempt to unify sublocale and interpretation into global theories
2015-11-14 haftmann 2015-11-14 prefer "rewrites" and "defines" to note rewrite morphisms
2015-09-15 nipkow 2015-09-15 goali -> i
2014-02-19 haftmann 2014-02-19 more convenient syntax for permanent interpretation
2014-02-19 haftmann 2014-02-19 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
2014-02-07 nipkow 2014-02-07 fight spurious nitpick timeouts
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-07-03 nipkow 2013-07-03 tuned names
2013-05-16 nipkow 2013-05-16 finally: acom with pointwise access and update of annotations
2013-05-14 nipkow 2013-05-14 tuned names
2013-05-13 nipkow 2013-05-13 tuned names
2013-05-09 nipkow 2013-05-09 standard ivl notation [l,h]
2013-05-08 nipkow 2013-05-08 tuned
2013-05-07 nipkow 2013-05-07 tuned name: filter -> constrain (longer but more intuitive)
2013-04-30 nipkow 2013-04-30 canonical names of classes
2013-04-26 nipkow 2013-04-26 simplified def
2013-04-26 nipkow 2013-04-26 more standard argument order
2013-04-26 nipkow 2013-04-26 simplified def
2013-04-26 nipkow 2013-04-26 more standard order of arguments
2013-04-20 nipkow 2013-04-20 proved termination for fun-based AI
2013-04-17 nipkow 2013-04-17 complete revision: finally got rid of annoying L-predicate
2013-03-11 nipkow 2013-03-11 more factorisation of Step & Co
2013-03-10 nipkow 2013-03-10 termination proof for narrowing: fewer assumptions
2013-03-08 nipkow 2013-03-08 simplified basic termination proof
2013-03-06 nipkow 2013-03-06 major redesign: order instead of preorder, new definition of intervals as quotients
2013-02-22 nipkow 2013-02-22 more abstract intervals
2013-02-12 nipkow 2013-02-12 tuned top
2013-01-25 nipkow 2013-01-25 tuned
2013-01-19 nipkow 2013-01-19 simplified proofs
2012-10-17 wenzelm 2012-10-17 proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
2012-09-26 nipkow 2012-09-26 tuned
2012-09-26 nipkow 2012-09-26 added counterexamples
2012-09-25 nipkow 2012-09-25 tuned
2012-09-24 nipkow 2012-09-24 generalized types
2012-09-24 nipkow 2012-09-24 tuned termination proof
2012-09-21 nipkow 2012-09-21 more termination proofs
2012-09-17 nipkow 2012-09-17 tuned
2012-09-16 nipkow 2012-09-16 converted wt into a set, tuned names
2012-09-07 nipkow 2012-09-07 adjusted examples
2012-09-03 nipkow 2012-09-03 added annotations after condition in if and while
2012-08-10 nipkow 2012-08-10 Improved complete lattice formalisation - no more index set.
2012-04-19 nipkow 2012-04-19 added revised version of Abs_Int