src/CCL/Wfd.thy
Mon, 23 May 2016 21:30:30 +0200 wenzelm embedded content may be delimited via cartouches;
Tue, 29 Dec 2015 22:03:02 +0100 wenzelm more symbols;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Mon, 23 Mar 2015 13:30:59 +0100 wenzelm support 'for' fixes in rule_tac etc.;
Fri, 20 Mar 2015 14:48:04 +0100 wenzelm tuned signature;
Thu, 19 Mar 2015 22:30:57 +0100 wenzelm more position information;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 16:46:21 +0100 wenzelm misc tuning;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Tue, 11 Nov 2014 15:55:31 +0100 wenzelm more symbols;
Tue, 11 Nov 2014 13:50:56 +0100 wenzelm tuned whitespace;
Tue, 11 Nov 2014 13:44:09 +0100 wenzelm more markup;
Tue, 11 Nov 2014 10:54:52 +0100 wenzelm more Isar proof methods;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 16 Aug 2014 11:35:33 +0200 wenzelm prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
Sat, 05 Jul 2014 13:39:53 +0200 wenzelm modernized definitions;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Wed, 23 May 2012 15:57:12 +0200 wenzelm eliminated obsolete fastsimp;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Wed, 12 Jan 2011 16:33:04 +0100 wenzelm eliminated global prems;
Tue, 17 Aug 2010 19:36:39 +0200 haftmann more antiquotations
Fri, 23 Apr 2010 23:35:43 +0200 wenzelm mark schematic statements explicitly;
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