src/FOL/FOL.thy
Fri, 19 Jun 2020 09:46:47 +0000 haftmann prefer single name
Thu, 04 Jun 2020 15:30:22 +0000 haftmann activate simproc for FOL
Thu, 04 Jun 2020 15:30:22 +0000 haftmann more rules for FOL also
Sun, 24 May 2020 19:57:13 +0000 haftmann better closeup and more consistent terminology
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 03 Jan 2019 22:19:19 +0100 wenzelm isabelle update_inner_syntax_cartouches;
Mon, 23 May 2016 21:30:30 +0200 wenzelm embedded content may be delimited via cartouches;
Fri, 01 Jan 2016 10:49:00 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 19 Oct 2015 20:29:29 +0200 wenzelm more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Thu, 09 Apr 2015 20:42:32 +0200 wenzelm clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
Mon, 06 Apr 2015 23:54:13 +0200 wenzelm tuned;
Mon, 06 Apr 2015 23:14:05 +0200 wenzelm local setup of induction tools, with restricted access to auxiliary consts;
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;
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;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Thu, 30 May 2013 16:48:50 +0200 wenzelm tuned import;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 17:17:16 +0200 wenzelm discontinued obsolete ML antiquotation @{claset};
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
less more (0) -100 -50 -30 tip