src/FOL/FOL.thy
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;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 20 Nov 2011 13:29:12 +0100 wenzelm tuned;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sun, 15 May 2011 17:45:53 +0200 wenzelm simplified/unified method_setup/attribute_setup;
Sat, 14 May 2011 13:32:33 +0200 wenzelm simplified BLAST_DATA;
Sat, 14 May 2011 11:42:43 +0200 wenzelm modernized functor names;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Tue, 26 Apr 2011 21:27:01 +0200 wenzelm simplified Blast setup;
Fri, 22 Apr 2011 15:05:04 +0200 wenzelm misc tuning and simplification;
Fri, 22 Apr 2011 14:30:32 +0200 wenzelm proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
Fri, 22 Apr 2011 13:58:13 +0200 wenzelm modernized Quantifier1 simproc setup;
Fri, 22 Apr 2011 12:46:48 +0200 wenzelm clarified simpset setup;
Wed, 23 Feb 2011 11:23:26 +0100 noschinl setup case_product attribute in HOL and FOL
Fri, 18 Feb 2011 17:03:30 +0100 wenzelm modernized specifications;
Mon, 20 Dec 2010 16:44:33 +0100 wenzelm proper identifiers for consts and types;
Wed, 12 May 2010 16:44:49 +0200 wenzelm modernized specifications;
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Sat, 30 Jan 2010 17:01:01 +0100 berghofe Adapted to changes in setup of cases method.
Sun, 10 Jan 2010 18:41:07 +0100 berghofe Adapted to changes in setup of induct method.
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 29 Jul 2009 00:09:14 +0200 wenzelm removed old global get_claset/map_claset;
Fri, 24 Jul 2009 21:21:45 +0200 wenzelm renamed functor BlastFun to Blast, require explicit theory;
Fri, 24 Jul 2009 12:33:00 +0200 wenzelm renamed functor InductFun to Induct;
Thu, 09 Jul 2009 22:09:58 +0200 wenzelm removed obsolete CVS Ids;
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Thu, 20 Nov 2008 00:03:47 +0100 wenzelm Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
Tue, 28 Oct 2008 11:03:07 +0100 ballarin Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Wed, 13 Aug 2008 20:57:18 +0200 wenzelm tuned document;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
less more (0) -100 -60 tip