| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Mon, 08 Nov 2021 19:56:15 +0100 |
nipkow |
added eq_iff_swap for creating symmetric variants of thms; applied it in List.
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 21:20:15 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:14:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2020 12:10:58 +0000 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Fri, 19 Jun 2020 09:46:47 +0000 |
haftmann |
prefer single name
|
file |
diff |
annotate
|
| Thu, 04 Jun 2020 15:30:22 +0000 |
haftmann |
more simp rules
|
file |
diff |
annotate
|
| Sat, 30 May 2020 08:50:18 +0000 |
haftmann |
install simproc but deactivate by default
|
file |
diff |
annotate
|
| Sun, 24 May 2020 19:57:13 +0000 |
haftmann |
better closeup and more consistent terminology
|
file |
diff |
annotate
|
| Wed, 13 May 2020 16:35:36 +0200 |
Manuel Eberl |
new HOL simproc: eliminate_false_implies
|
file |
diff |
annotate
|
| Tue, 12 May 2020 15:11:20 +0100 |
paulson |
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Sat, 28 Mar 2020 17:27:01 +0000 |
paulson |
structured a lot of ancient, horrible proofs
|
file |
diff |
annotate
|
| Tue, 03 Mar 2020 19:26:23 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 13:30:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Oct 2019 16:26:31 +0200 |
wenzelm |
clarified sessions/directories;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 18:41:12 +0200 |
wenzelm |
setup preprocessing for HOL proofs;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 16:46:33 +0200 |
wenzelm |
early setup of proof preprocessing;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2019 18:23:32 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 20:49:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Wed, 12 Sep 2018 17:12:33 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Tue, 11 Sep 2018 16:21:54 +0100 |
paulson |
A few new results, elimination of duplicates and more use of "pairwise"
|
file |
diff |
annotate
|
| Wed, 12 Sep 2018 16:12:50 +0200 |
nipkow |
tuned "=" syntax declarations; made "~=" uniformly "infix"
|
file |
diff |
annotate
|
| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:54:55 +0000 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 19:17:52 +0100 |
wenzelm |
prefer formal citations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 22 Oct 2017 09:10:10 +0200 |
nipkow |
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Sat, 17 Jun 2017 15:41:19 +0200 |
nipkow |
added simp rules
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 17:59:28 +0200 |
wenzelm |
clarified notation: iterated quantifier is negated as one chunk;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 15:16:42 +0200 |
wenzelm |
clarified notation;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2016 22:11:29 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 20:47:31 +0100 |
wenzelm |
abbreviations for \<nexists>;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 19:58:56 +0100 |
wenzelm |
old HOL syntax is for input only;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 11:49:35 +0100 |
wenzelm |
eliminated old defs;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 17:16:21 +0100 |
wenzelm |
discontinued ASCII replacement syntax <->;
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 15:39:01 +0100 |
haftmann |
stripped some legacy
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 21:46:14 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 11:31:56 +0200 |
nipkow |
Added new simplifier predicate ASSUMPTION
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 23:41:53 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 11:40:43 +0200 |
wenzelm |
proper LaTeX;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2015 00:03:10 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sat, 09 May 2015 12:19:24 +0200 |
nipkow |
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
|
file |
diff |
annotate
|
| Sun, 03 May 2015 15:38:25 +0200 |
nipkow |
swap False to the right in assumptions to be eliminated at the right end
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 19:09:28 +0200 |
nipkow |
undid 6d7b7a037e8d
|
file |
diff |
annotate
|
| Sat, 25 Apr 2015 17:38:22 +0200 |
nipkow |
new ==> simp rule
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 12:11:48 +0200 |
nipkow |
added simp rules for ==>
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 12:37:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:29:44 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 15:08:02 +0100 |
hoelzl |
fix parameter order of NO_MATCH
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:14:41 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 12:01:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 16:08:11 +0000 |
paulson |
New lemmas and a bit of tidying up.
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 16:46:21 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sat, 22 Nov 2014 11:36:00 +0100 |
wenzelm |
named_theorems: multiple args;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 18:27:43 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 09:15:54 +0100 |
hoelzl |
disable coercions for NO_MATCH
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:49 +0200 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 22:14:57 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 21:11:08 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 20:46:59 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 13:23:50 +0200 |
wenzelm |
modernized module name and setup;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 12 May 2014 17:17:32 +0200 |
wenzelm |
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 10:51:22 +0200 |
blanchet |
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 20:19:41 +0100 |
wenzelm |
modernized tool setup;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 21:03:28 +0100 |
wenzelm |
more explicit axiomatization;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:09:53 +0100 |
wenzelm |
more standard file/module names;
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:48 +0100 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 21:15:43 +0200 |
haftmann |
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
|
file |
diff |
annotate
|
| Sun, 14 Jul 2013 00:08:15 +0200 |
wenzelm |
recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 00:50:49 +0200 |
wenzelm |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 22:31:50 +0200 |
wenzelm |
tuned message -- more markup;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 21:20:35 +0200 |
wenzelm |
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 19:14:47 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:17:16 +0200 |
wenzelm |
discontinued obsolete ML antiquotation @{claset};
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 14:33:45 +0100 |
traytel |
separate data used for case translation from the datatype package
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:54:52 +0100 |
wenzelm |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 13:24:51 +0100 |
wenzelm |
marginalized historic strip_tac;
|
file |
diff |
annotate
|
| Wed, 06 Feb 2013 17:18:01 +0100 |
hoelzl |
check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 11:05:23 +0100 |
nipkow |
\<noteq> now has the same associativity as ~= and =
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 22:00:29 +0200 |
wenzelm |
eliminated some old material that is unused in the visible universe;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2012 16:58:03 +0200 |
wenzelm |
removed obsolete rev_contrapos (cf. 1d195de59497);
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:10:51 +0200 |
haftmann |
prefer sys.error over plain error in Scala to avoid deprecation warning
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:36:24 +0200 |
haftmann |
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:31:19 +0100 |
wenzelm |
modernized axiomatization;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 11 Jan 2012 21:04:22 +0100 |
wenzelm |
more conventional eval_tac vs. method_setup "eval";
|
file |
diff |
annotate
|
| Mon, 09 Jan 2012 18:29:42 +0100 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 18:18:39 +0100 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:16 +0200 |
bulwahn |
removing old code generator setup in the HOL theory
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 22:48:23 +0200 |
wenzelm |
modernized structure Induct_Tacs;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:25:17 +0200 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 13:59:59 +0200 |
bulwahn |
removing the SML evaluator
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 13:32:33 +0200 |
wenzelm |
simplified BLAST_DATA;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 11:42:43 +0200 |
wenzelm |
modernized functor names;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 21:27:01 +0200 |
wenzelm |
simplified Blast setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 15:05:04 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 14:30:32 +0200 |
wenzelm |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 12:46:48 +0200 |
wenzelm |
clarified simpset setup;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 14:33:33 +0200 |
wenzelm |
explicit context for Codegen.eval_term etc.;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 11:21:12 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 07:44:23 +0200 |
bulwahn |
making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 09:43:36 +0200 |
haftmann |
corrected infix precedence for boolean operators in Haskell
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 15:06:36 +0000 |
paulson |
declare ext [intro]: Extensionality now available by default
|
file |
diff |
annotate
|
| Wed, 23 Feb 2011 11:23:26 +0100 |
noschinl |
setup case_product attribute in HOL and FOL
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Thu, 27 Jan 2011 16:24:29 +0100 |
wenzelm |
CRITICAL markup for critical poking with unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:33:35 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:56 +0100 |
blanchet |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:25:05 +0100 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 18:00:40 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:33:17 +0100 |
haftmann |
file for package tool type_mapper carries the same name as its Isar command
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 14:56:07 +0100 |
wenzelm |
simplified HOL.eq simproc matching;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 17:54:15 +0100 |
wenzelm |
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 11:09:18 +0100 |
haftmann |
module for functorial mappers
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 19:14:33 +0200 |
blanchet |
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 11:02:24 +0200 |
krauss |
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 12:01:04 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 09:17:24 +0200 |
blanchet |
comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 11:11:59 +0200 |
haftmann |
corrected OCaml operator precedence
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 18:43:18 +0200 |
haftmann |
Pure equality is a regular cpde operation
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:33 +0200 |
haftmann |
adjusted to changes in Code_Runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 20:47:14 +0200 |
wenzelm |
dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 16:47:31 +0200 |
haftmann |
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:40:35 +0200 |
haftmann |
Code_Runtime.value, corresponding to ML_Context.value
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:31:32 +0200 |
haftmann |
code_eval renamed to code_runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 11:30:32 +0200 |
haftmann |
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 16:36:23 +0200 |
blanchet |
added Auto Try to the mix of automatic tools
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:45:39 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:29:02 +0200 |
blanchet |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:42:50 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:29:47 +0200 |
haftmann |
avoid cyclic modules
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 09:13:28 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 09:13:16 +0200 |
haftmann |
normalization is allowed to solve True
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:51:16 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:29:30 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 00:03:15 +0200 |
blanchet |
finish moving file
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:40:25 +0200 |
haftmann |
normalization fails on unchanged goal
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:01:12 +0200 |
haftmann |
tuned text segment
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 21:01:47 +0200 |
blanchet |
fiddling with "try"
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 09:37:43 +0200 |
haftmann |
hide all-too-popular constant name eq
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 12:19:49 +0200 |
haftmann |
prevent line breaks after Scala symbolic operators
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 14:18:09 +0200 |
wenzelm |
discontinued obsolete 'global' and 'local' commands;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:49 +0200 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:03:07 +0200 |
haftmann |
deglobalized named HOL constants
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 10:27:02 +0200 |
haftmann |
tuned declaration order
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 14:55:09 +0200 |
haftmann |
qualified constants Let and If
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
optional break
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 10:38:29 +0200 |
haftmann |
dropped unused bindings
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 15:38:47 +0200 |
blanchet |
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:15:21 +0200 |
wenzelm |
just one version of Thm.unconstrainT, which affects all variables;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:10:42 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 04 May 2010 12:26:46 +0200 |
berghofe |
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:41 +0200 |
haftmann |
avoid popular infixes
|
file |
diff |
annotate
|