src/HOL/IMP/Abs_Int1_const.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-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
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"
2013-07-03 nipkow 2013-07-03 tuned names
2013-04-30 nipkow 2013-04-30 canonical names of classes
2013-04-29 nipkow 2013-04-29 tuned
2013-04-29 nipkow 2013-04-29 tuned
2013-04-29 nipkow 2013-04-29 tuned
2013-04-17 nipkow 2013-04-17 complete revision: finally got rid of annoying L-predicate
2013-03-10 nipkow 2013-03-10 factored out Step
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-12 nipkow 2013-02-12 tuned top
2013-01-25 nipkow 2013-01-25 tuned
2012-09-18 nipkow 2012-09-18 tuned
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-04-19 nipkow 2012-04-19 added revised version of Abs_Int