Tue, 10 Jun 2008 21:50:30 +0200 wenzelm fixed spelling (Where is WordExamples.thy anyway?);
Tue, 10 Jun 2008 21:50:05 +0200 wenzelm recovered nat_induct as default for induct_tac;
Tue, 10 Jun 2008 21:49:37 +0200 wenzelm more robust declaration of nat_induct;
Tue, 10 Jun 2008 21:49:11 +0200 wenzelm reordering of imports ensures that nat_induct stay in front;
Tue, 10 Jun 2008 19:45:53 +0200 wenzelm adhoc fix of induct_tac: rule nat_induct;
Tue, 10 Jun 2008 19:34:32 +0200 wenzelm case_tac: accomodate change in bound variable name;
Tue, 10 Jun 2008 19:15:23 +0200 wenzelm nat_induct_tac (works without context);
Tue, 10 Jun 2008 19:15:23 +0200 wenzelm moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;
Tue, 10 Jun 2008 19:15:21 +0200 wenzelm added nat_induct_tac (works without context);
Tue, 10 Jun 2008 19:15:21 +0200 wenzelm InductTacs.case_tac with proper context and proper declaration of local variable;
Tue, 10 Jun 2008 19:15:20 +0200 wenzelm added HOL/Tools/induct_tacs.ML;
Tue, 10 Jun 2008 19:15:19 +0200 wenzelm eliminated obsolete case_split_thm -- use case_split;
Tue, 10 Jun 2008 19:15:18 +0200 wenzelm tuned proofs -- case_tac *is* available here;
Tue, 10 Jun 2008 19:15:17 +0200 wenzelm updated generated file;
Tue, 10 Jun 2008 19:15:16 +0200 wenzelm case_tac/induct_tac: use same declarations as cases/induct;
Tue, 10 Jun 2008 19:15:14 +0200 wenzelm proper news header;
Tue, 10 Jun 2008 16:43:26 +0200 wenzelm removed obsolete read_idents;
Tue, 10 Jun 2008 16:43:23 +0200 wenzelm added (e)res_inst_tac;
Tue, 10 Jun 2008 16:43:21 +0200 wenzelm focus: actually declare constraints for local parameters;
Tue, 10 Jun 2008 16:43:16 +0200 wenzelm tuned proofs;
Tue, 10 Jun 2008 16:43:14 +0200 wenzelm case_split_tac (works without context);
Tue, 10 Jun 2008 16:43:07 +0200 wenzelm tuned;
Tue, 10 Jun 2008 16:43:01 +0200 wenzelm eliminated obsolete case_split_thm -- use case_split;
Tue, 10 Jun 2008 16:42:38 +0200 wenzelm Unstructured induction and cases analysis for Isabelle/HOL.
Tue, 10 Jun 2008 15:31:05 +0200 haftmann dropped instance with attached definitions
Tue, 10 Jun 2008 15:31:04 +0200 haftmann polished interface of datatype package
Tue, 10 Jun 2008 15:31:03 +0200 haftmann adjusted some proofs involving inats
Tue, 10 Jun 2008 15:31:02 +0200 haftmann refactoring; addition, numerals
Tue, 10 Jun 2008 15:31:01 +0200 haftmann more instantiation
Tue, 10 Jun 2008 15:30:59 +0200 haftmann whitespace tuning
Tue, 10 Jun 2008 15:30:58 +0200 haftmann localized Least in Orderings.thy
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Tue, 10 Jun 2008 15:30:54 +0200 haftmann slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
Tue, 10 Jun 2008 15:30:33 +0200 haftmann rep_datatype command now takes list of constructors as input arguments
Tue, 10 Jun 2008 15:30:06 +0200 haftmann major refactorings in code generator modules
Tue, 10 Jun 2008 15:30:01 +0200 haftmann updated
Tue, 10 Jun 2008 14:32:58 +0200 haftmann slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
Mon, 09 Jun 2008 17:39:35 +0200 wenzelm DatatypePackage.case_tac;
Mon, 09 Jun 2008 17:31:25 +0200 wenzelm DatatypePackage.distinct_simproc;
Mon, 09 Jun 2008 17:24:48 +0200 wenzelm DatatypePackage.case_tac;
Mon, 09 Jun 2008 17:07:11 +0200 wenzelm signature cleanup -- no pervasives anymore;
Mon, 09 Jun 2008 17:07:10 +0200 wenzelm qualified DatatypePackage.distinct_simproc;
Mon, 09 Jun 2008 17:07:08 +0200 wenzelm adapted case_tac/induct_tac;
Sun, 08 Jun 2008 14:31:06 +0200 wenzelm updated generated file; Isabelle2008
Sun, 08 Jun 2008 14:30:46 +0200 wenzelm minor typos;
Sun, 08 Jun 2008 14:30:07 +0200 wenzelm simp: depth_limit is now a configuration option;
Sun, 08 Jun 2008 14:29:36 +0200 wenzelm removed old AxClass;
Sun, 08 Jun 2008 14:29:09 +0200 wenzelm remove codegen_process.pdf from distribution;
Sat, 07 Jun 2008 19:18:38 +0200 haftmann fixed wrong treatment of type variables in instantiation target
Fri, 06 Jun 2008 18:36:35 +0200 wenzelm switched to Poly/ML 5.2;
Fri, 06 Jun 2008 08:52:35 +0200 isatest doc test now runs on linux
Thu, 05 Jun 2008 14:28:02 +0200 wenzelm added at-poly-5.1-para-e;
Thu, 05 Jun 2008 12:03:48 +0200 haftmann adjusted location of cambridge website
Thu, 05 Jun 2008 09:01:17 +0200 isatest switch from gtar to tar
Thu, 05 Jun 2008 00:52:22 +0200 isatest send from linux systems as well
Wed, 04 Jun 2008 17:12:00 +0200 wenzelm tikz: change to pgfsys-dvi.def for plain dvi output;
Wed, 04 Jun 2008 16:44:31 +0200 wenzelm replaced (*<*)(*>*) by invisibility tags;
Wed, 04 Jun 2008 16:44:08 +0200 wenzelm updated generated file;
Wed, 04 Jun 2008 16:32:24 +0200 wenzelm updated generated file;
Wed, 04 Jun 2008 16:32:14 +0200 wenzelm work within *this* directory;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip