src/CCL/Wfd.thy
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Thu, 30 Jul 2009 11:23:57 +0200 wenzelm FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
Sun, 26 Jul 2009 19:54:37 +0200 wenzelm tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Wed, 31 Dec 2008 00:08:11 +0100 wenzelm use regular Term.add_vars, Term.add_frees etc.;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Sat, 14 Jun 2008 23:52:51 +0200 wenzelm proper context for tactics derived from res_inst_tac;
Sat, 14 Jun 2008 23:19:51 +0200 wenzelm proper context for tactics derived from res_inst_tac;
Wed, 11 Jun 2008 15:40:20 +0200 wenzelm more antiquotations;
Tue, 25 Mar 2008 19:39:57 +0100 wenzelm more antiquotations;
Wed, 03 Oct 2007 21:29:05 +0200 wenzelm avoid unnamed infixes;
Sun, 29 Jul 2007 14:29:48 +0200 wenzelm simplified "eval" setup via NamedThmsFun;
Thu, 21 Jun 2007 22:10:16 +0200 wenzelm tuned proofs -- avoid implicit prems;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Tue, 25 Jul 2006 21:17:58 +0200 wenzelm Drule.merge_rules;
Tue, 18 Jul 2006 02:22:38 +0200 wenzelm removed obsolete ML files;
Sat, 17 Sep 2005 17:35:26 +0200 wenzelm converted to Isar theory format;
Fri, 10 Oct 1997 17:10:12 +0200 wenzelm fixed dots;
Mon, 05 Feb 1996 14:44:09 +0100 clasohm expanded tabs
Tue, 22 Mar 1994 12:42:56 +0100 clasohm changed "." to "$" to eliminate ambiguity
Fri, 14 Jan 1994 12:42:49 +0100 lcp corrected comments
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip