| Wed, 17 Sep 2025 12:19:12 +0100 |
paulson |
two new theorems
|
file |
diff |
annotate
|
| Thu, 07 Aug 2025 21:40:03 +0200 |
wenzelm |
avoid legacy operations;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2025 13:06:42 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
|
file |
diff |
annotate
|
| Thu, 12 Jun 2025 12:59:17 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 24 May 2025 09:06:26 +0200 |
haftmann |
move legacy simplifier interfaces into separate file
|
file |
diff |
annotate
|
| Wed, 21 May 2025 20:44:12 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 27 Mar 2025 16:35:41 +0100 |
desharna |
tuned signature
|
file |
diff |
annotate
|
| Thu, 27 Mar 2025 14:33:08 +0100 |
desharna |
tuned and moved configuration of auto_try0 to theory HOL
|
file |
diff |
annotate
|
| Thu, 27 Mar 2025 13:30:16 +0100 |
desharna |
moved try0's HOL-specific stuff into own theory
|
file |
diff |
annotate
|
| Wed, 22 Jan 2025 22:22:19 +0100 |
wenzelm |
misc tuning: more concise operations on prems (without change of exceptions);
|
file |
diff |
annotate
|
| Thu, 02 Jan 2025 08:37:55 +0100 |
haftmann |
refined syntax for code_reserved
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 14:59:57 +0100 |
wenzelm |
more syntax bundles, e.g. to explore terms without notation;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 19:00:19 +0200 |
wenzelm |
more type information;
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 12:10:35 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Tue, 01 Oct 2024 21:30:59 +0200 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Thu, 26 Sep 2024 14:44:37 +0100 |
paulson |
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 21:09:23 +0200 |
wenzelm |
more inner syntax markup: HOL;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:11:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:02:19 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 18:53:24 +0200 |
wenzelm |
tuned: prefer canonical argument order;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2024 15:37:27 +0200 |
wenzelm |
tuned (see also db120661dded);
|
file |
diff |
annotate
|
| Wed, 07 Aug 2024 15:11:54 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2024 21:21:02 +0200 |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 14:32:50 +0000 |
paulson |
Moving valuable library material from Martingales into the distribution
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 17:06:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 16:31:17 +0200 |
wenzelm |
clarified syntax and order of parameters;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 22:29:12 +0200 |
wenzelm |
clarified simproc_setup (passive);
|
file |
diff |
annotate
|
| Tue, 23 May 2023 21:43:36 +0200 |
wenzelm |
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 20:21:33 +0100 |
wenzelm |
isabelle update -u cite -l "";
|
file |
diff |
annotate
|
| 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
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 09:45:22 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 09:26:31 -0700 |
huffman |
syntax precedence for If and Let
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 23:09:32 +0200 |
wenzelm |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:36:04 +0200 |
wenzelm |
removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 14:49:53 +0200 |
blanchet |
reintroduce efficient set structure to collect "no_atp" theorems
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:01:01 +0100 |
blanchet |
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:14:43 +0100 |
blanchet |
added support for "specification" and "ax_specification" constructs to Nitpick
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:42:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 21:43:26 +0100 |
wenzelm |
tuned hyp_subst_tac';
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Sun, 31 Jan 2010 15:22:40 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
| Sat, 30 Jan 2010 16:59:49 +0100 |
berghofe |
Added setup for simplification of equality constraints in cases rules.
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Fri, 15 Jan 2010 14:43:00 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:03:20 +0100 |
berghofe |
Added setup for simplification of equality constraints in induction rules.
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 08:56:15 +0100 |
haftmann |
some syntax setup for Scala
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 16:45:02 +0100 |
haftmann |
tuned code equations
|
file |
diff |
annotate
|
| Fri, 08 Jan 2010 14:34:17 +0100 |
haftmann |
boolean operators for scala
|
file |
diff |
annotate
|
| Fri, 08 Jan 2010 12:25:15 +0100 |
haftmann |
a primitive scala serializer
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:19:33 +0100 |
wenzelm |
some rearangement of load order to keep preferences adjacent -- slightly fragile;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 15:33:35 +0100 |
wenzelm |
removed unused Quickcheck_RecFun_Simps;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:06:15 +0100 |
wenzelm |
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 10:51:41 +0100 |
haftmann |
tuned code setup for primitive boolean connectors
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 17:12:36 +0200 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 15:02:48 +0100 |
paulson |
Removal of the unused atpset concept, the atp attribute and some related code.
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 23:13:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 22:47:34 +0200 |
wenzelm |
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 11:40:28 +0200 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:21:45 +0200 |
wenzelm |
renamed functor BlastFun to Blast, require explicit theory;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 18:58:58 +0200 |
wenzelm |
renamed functor ProjectRuleFun to Project_Rule;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 12:33:00 +0200 |
wenzelm |
renamed functor InductFun to Induct;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 14:36:26 +0200 |
haftmann |
moved abstract algebra section to the end
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:31 +0200 |
haftmann |
tuned code annotations
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:21:26 +0200 |
haftmann |
more accurate certificates for constant aliasses
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2009 14:59:29 +0200 |
haftmann |
arbitrary farewell
|
file |
diff |
annotate
|
| Sat, 30 May 2009 12:52:57 +0200 |
wenzelm |
modernized method setup;
|
file |
diff |
annotate
|
| Sat, 16 May 2009 15:24:35 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Sat, 16 May 2009 15:23:52 +0200 |
bulwahn |
added collection of simplification rules of recursive functions for quickcheck
|
file |
diff |
annotate
|
| Sat, 16 May 2009 11:28:02 +0200 |
nipkow |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Thu, 14 May 2009 09:16:34 +0200 |
haftmann |
rewrite op = == eq handled by simproc
|
file |
diff |
annotate
|
| Wed, 13 May 2009 18:41:35 +0200 |
haftmann |
itself is instance of eq
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:15:01 -0700 |
huffman |
reimplement reorientation simproc using theory data
|
file |
diff |
annotate
|
| Sat, 25 Apr 2009 21:28:04 +0200 |
wenzelm |
misc cleanup of auto_solve and quickcheck:
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 08:24:54 +0200 |
haftmann |
generic postprocessing scheme for term evaluations
|
file |
diff |
annotate
|
| Thu, 23 Apr 2009 12:17:50 +0200 |
haftmann |
avoid local [code]
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 14:29:56 +0200 |
haftmann |
re-engineering of evaluation conversions
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:52:37 +0200 |
haftmann |
code generator bootstrap theory src/Tools/Code_Generator.thy
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:34:54 +0200 |
haftmann |
wrecked old code_funcgr module
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 17:05:40 +0100 |
blanchet |
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 15:31:07 +0100 |
blanchet |
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 18:18:05 +0100 |
blanchet |
Second try at adding "nitpick_const_def" attribute.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 18:40:16 +0100 |
blanchet |
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:58:39 +0100 |
haftmann |
reduced confusion code_funcgr vs. code_wellsorted
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:52:21 +0100 |
wenzelm |
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:02:12 +0100 |
wenzelm |
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 22:32:50 +0100 |
haftmann |
experimental switch to new well-sorting algorithm
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 10:22:29 +0100 |
haftmann |
formal dependency on newly emerging algorithm
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 14:49:24 +0100 |
haftmann |
reverted to old wellsorting algorithm
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 10:14:31 +0100 |
haftmann |
experimental inclusion of new wellsorting algorithm for code equations
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:18:31 +0100 |
haftmann |
do not drop arguments to 0, 1
|
file |
diff |
annotate
|
| Tue, 10 Feb 2009 14:02:45 +0100 |
blanchet |
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 12:31:36 +0100 |
blanchet |
Reintroduced nitpick_ind_intro attribute.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 10:37:59 +0100 |
blanchet |
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:57:47 +0100 |
blanchet |
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:29:11 +0100 |
haftmann |
added HOL-Base image
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 09:58:45 +0100 |
haftmann |
moved value.ML to src/Tools
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 15:58:38 +0100 |
haftmann |
simproc for let
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:34 +0200 |
haftmann |
"arbitrary" merely abbreviates undefined
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:45 +0200 |
haftmann |
code identifier namings are no longer imperative
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:16 +0200 |
haftmann |
re-introduces axiom subst
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:31:57 +0200 |
haftmann |
polished code generator setup
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 23:00:15 +0200 |
berghofe |
Added setup for coherent logic prover.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:22 +0200 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:24:29 +0200 |
haftmann |
tuned code generator setup
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:47:18 +0200 |
krauss |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:14 +0200 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 15:51:38 +0200 |
wenzelm |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:20:03 +0200 |
wenzelm |
removed obsolete case_split_tac -- cannot work without;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:19 +0200 |
wenzelm |
eliminated obsolete case_split_thm -- use case_split;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:58 +0200 |
haftmann |
localized Least in Orderings.thy
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2008 16:53:04 +0200 |
haftmann |
moved 'trivial classes' to foundation of code generator
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 22:00:25 +0200 |
haftmann |
different handling of eq class for nbe
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:13 +0200 |
wenzelm |
Sign.hide_const;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 18:30:40 +0200 |
krauss |
Generic conversion and tactic "atomize_elim" to convert elimination rules
|
file |
diff |
annotate
|
| Fri, 04 Apr 2008 13:40:21 +0200 |
haftmann |
postprocessing of equality
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:01 +0100 |
wenzelm |
pass imp_elim, swap to classical prover;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Sat, 22 Dec 2007 14:10:22 +0100 |
wenzelm |
use random_word.ML earlier;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:44:18 +0100 |
wenzelm |
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:33 +0100 |
haftmann |
interpretation of typedecls: instantiation to class type
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:00:05 +0100 |
wenzelm |
tuned specifications of 'notation';
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 22:50:00 +0100 |
kleing |
move itself into HOL types
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 08:04:28 +0200 |
haftmann |
added first version of user-space type system for class target
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:54:44 +0200 |
haftmann |
certificates for code generator case expressions
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:42:03 +0200 |
haftmann |
clarified declarations in class ord
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:34 +0200 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 17:56:03 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:24:34 +0200 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
| Thu, 16 Aug 2007 11:45:06 +0200 |
haftmann |
fixed codegen setup
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:49 +0200 |
wenzelm |
simplified ResAtpset via NamedThmsFun;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 16:49:34 +0200 |
wenzelm |
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 22:27:05 +0200 |
wenzelm |
use hologic.ML in basic HOL context;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2007 19:09:32 +0200 |
haftmann |
simplified keyword setup
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:22 +0200 |
chaieb |
added Theorem all_not_ex
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 19:23:09 +0200 |
haftmann |
tuned boostrap
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
| Thu, 31 May 2007 20:55:29 +0200 |
wenzelm |
moved IsaPlanner from Provers to Tools;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:51 +0200 |
wenzelm |
proper loading of ML files;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 19:08:42 +0200 |
chaieb |
added a set of NNF normalization lemmas and nnf_conv
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:24 +0200 |
haftmann |
dropped HOL.ML
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:38 +0100 |
haftmann |
added class "default" and expansion axioms for undefined
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
| Sun, 18 Mar 2007 01:50:05 +0100 |
dixon |
TrueElim and notTrueElim tested and added as safe elim rules.
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 16:40:49 +0100 |
dixon |
removed safe elim flag of trueElim and notFalseElim for testing.
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 16:37:52 +0100 |
dixon |
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:43 +0100 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2007 16:05:10 +0100 |
haftmann |
dropped lemma duplicates in HOL.thy
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:12 +0100 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:42 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:39 +0100 |
haftmann |
moved order arities for fun and bool to Fun/Orderings
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:16 +0100 |
wenzelm |
updated (binder) syntax/notation;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:28 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:34:21 +0100 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 13:32:19 +0100 |
webertj |
typo in comment fixed
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:17 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 19:48:35 +0100 |
haftmann |
moved lemma eq_neq_eq_imp_neq to HOL
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 14:29:57 +0100 |
wenzelm |
tuned hypsubst setup;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Sun, 05 Nov 2006 21:44:32 +0100 |
wenzelm |
Sign.const_syntax_name;
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:37 +0100 |
haftmann |
simplified reasoning tools setup
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:55 +0100 |
haftmann |
added Equals_conv
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 12:32:44 +0200 |
haftmann |
lifted claset setup from ML to Isar level
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 14:51:24 +0200 |
haftmann |
cleaned up HOL bootstrap
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 10:35:24 +0200 |
haftmann |
cleanup basic HOL bootstrap
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:00:49 +0200 |
haftmann |
improved serialization for arbitrary
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 21:49:34 +0200 |
wenzelm |
proper const_syntax for uminus, abs;
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Mon, 25 Sep 2006 17:04:14 +0200 |
haftmann |
added 'undefined' serializer
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:44 +0200 |
haftmann |
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 21 Jul 2006 11:34:01 +0200 |
berghofe |
- Added new "undefined" constant
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 09:31:57 +0200 |
nipkow |
made evaluation_conv and normalization_conv visible.
|
file |
diff |
annotate
|
| Wed, 05 Jul 2006 16:24:28 +0200 |
paulson |
removed the "tagging" feature
|
file |
diff |
annotate
|
| Fri, 30 Jun 2006 18:26:22 +0200 |
nipkow |
normalization uses refl now
|
file |
diff |
annotate
|
| Thu, 29 Jun 2006 13:52:28 +0200 |
nipkow |
new method "normalization"
|
file |
diff |
annotate
|
| Wed, 14 Jun 2006 12:14:42 +0200 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 20:42:25 +0200 |
wenzelm |
quoted "if";
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|