src/HOL/Imperative_HOL/ex/Sublist.thy
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-04-08 bulwahn 2010-04-08 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-15 haftmann 2009-09-15 restored code generation for OCaml
2009-03-23 haftmann 2009-03-23 moved Imperative_HOL examples to Imperative_HOL/ex