src/HOL/UNITY/Simple/Reachability.thy
8 months ago haftmann 2018-11-18 removed legacy input syntax
17 months ago wenzelm 2018-02-15 more symbols;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-02-23 nipkow 2016-02-23 more canonical names
2012-03-13 wenzelm 2012-03-13 tuned proofs;
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-12-13 wenzelm 2011-12-13 modernized specifications;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-04-23 wenzelm 2011-04-23 modernized specifications;
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-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-05-07 berghofe 2008-05-07 - Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-02-05 paulson 2003-02-05 more tidying
2003-01-24 paulson 2003-01-24 Partial conversion of UNITY to Isar new-style theories
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-06 paulson 2001-08-06 Converted 1 to 1'
2001-03-05 paulson 2001-03-05 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp