src/FOL/IFOL.thy
Tue, 21 Sep 2021 13:14:18 +0200 wenzelm clarified antiquotations;
Sun, 27 Dec 2020 17:53:08 +0100 wenzelm tuned whitespace;
Fri, 19 Jun 2020 09:46:47 +0000 haftmann prefer single name
Thu, 04 Jun 2020 15:30:22 +0000 haftmann more rules for FOL also
Thu, 14 May 2020 10:26:33 +0100 paulson The Uniq quantifier for FOL too
Tue, 15 Oct 2019 13:34:50 +0200 wenzelm set_preproc for object-logics with type classes;
Sun, 28 Jul 2019 15:39:30 +0200 wenzelm purge remains from test (cf. 5a53724fe247);
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_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;
Thu, 03 Jan 2019 21:15:52 +0100 wenzelm isabelle update -u mixfix_cartouches;
Mon, 27 Aug 2018 14:42:24 +0200 wenzelm support named ML environments, notably "Isabelle", "SML";
Sat, 17 Sep 2016 11:41:13 +0200 Lars Hupel repair LaTeX dropout from f83ef97d8d7d
Fri, 16 Sep 2016 21:28:09 +0200 wenzelm more symbols;
Fri, 01 Jan 2016 10:49:00 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 19 Oct 2015 23:07:17 +0200 wenzelm repaired document;
Mon, 19 Oct 2015 20:29:29 +0200 wenzelm more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Wed, 11 Feb 2015 10:54:53 +0100 wenzelm proper context and method setup;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
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;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Sat, 16 Aug 2014 13:23:50 +0200 wenzelm modernized module name and setup;
Mon, 10 Feb 2014 17:20:11 +0100 wenzelm prefer vacuous definitional type classes over axiomatic ones;
Thu, 30 May 2013 16:48:50 +0200 wenzelm tuned import;
Thu, 30 May 2013 12:35:40 +0200 wenzelm standardized aliases;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Wed, 12 Sep 2012 22:00:29 +0200 wenzelm eliminated some old material that is unused in the visible universe;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Fri, 16 Mar 2012 22:22:05 +0100 wenzelm modernized axiomatization;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Sat, 14 May 2011 11:42:43 +0200 wenzelm modernized functor names;
Fri, 08 Apr 2011 23:33:57 +0200 wenzelm tuned;
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;
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Wed, 18 Aug 2010 12:26:48 +0200 haftmann deglobalization
Wed, 28 Apr 2010 12:07:52 +0200 wenzelm renamed command 'defaultsort' to 'default_sort';
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Sun, 28 Feb 2010 22:30:51 +0100 wenzelm more antiquotations;
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Sat, 30 May 2009 12:52:57 +0200 wenzelm modernized method setup;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sat, 28 Feb 2009 14:52:21 +0100 wenzelm moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
Sat, 28 Feb 2009 14:02:12 +0100 wenzelm moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
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, 24 Oct 2008 17:48:33 +0200 haftmann subst is a proper axiom again
Wed, 11 Jun 2008 18:01:11 +0200 wenzelm removed obsolete/unused pred_congs;
Wed, 11 Jun 2008 15:41:57 +0200 wenzelm tuned comments;
Sun, 18 May 2008 17:03:16 +0200 wenzelm setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
Tue, 08 Apr 2008 18:30:40 +0200 krauss Generic conversion and tactic "atomize_elim" to convert elimination rules
less more (0) -100 -60 tip