src/CTT/ex/Synthesis.thy
Sun, 09 Apr 2017 19:56:52 +0200 wenzelm clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;
Sat, 10 Oct 2015 21:43:07 +0200 wenzelm tuned syntax -- more symbols;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
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:40:13 +0100 wenzelm simplifie sessions;
Tue, 11 Nov 2014 11:41:58 +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, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 23 Apr 2010 23:35:43 +0200 wenzelm mark schematic statements explicitly;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Mon, 05 Jun 2006 21:54:20 +0200 wenzelm allow non-trivial schematic goals (via embedded term vars);
Fri, 02 Jun 2006 18:15:38 +0200 wenzelm removed obsolete ML files;
less more (0) tip