| Sun, 27 Dec 2015 17:16:21 +0100 |
wenzelm |
discontinued ASCII replacement syntax <->;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 13:33:42 +0200 |
wenzelm |
explicit indication of overloaded typedefs;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:44:57 +0100 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 11:32:32 +0100 |
wenzelm |
eliminated unused arith "verbose" flag -- tools that need options can use the context;
|
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
|
| Fri, 06 Feb 2015 17:57:03 +0100 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
cleaned up mess
|
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, 02 Nov 2014 16:54:06 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:37 +0200 |
blanchet |
moved old setup for SMT out
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:19 +0200 |
blanchet |
removed needless, and for (newer versions of?) Haskell problematic code equations
|
file |
diff |
annotate
|
| Sun, 27 Jul 2014 21:11:35 +0200 |
blanchet |
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
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
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Fri, 16 May 2014 16:40:02 +0200 |
noschinl |
added lemmas for -1
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 18:20:08 +0100 |
wenzelm |
repaired document;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 17:08:39 +0100 |
haftmann |
more precise imports;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 09:34:08 +0100 |
haftmann |
earlier setup of transfer, without dependency on psychodelic interpretations
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 08:21:46 +0100 |
haftmann |
cursory polishing: tuned proofs, tuned symbols, tuned headings
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 18:37:51 +0100 |
haftmann |
prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:22 +0100 |
haftmann |
dropped redundant lemma
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:21 +0100 |
haftmann |
syntactically tuned
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:20 +0100 |
haftmann |
prefer plain bool over dedicated type for binary digits
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 20:46:36 +0100 |
wenzelm |
more antiquotations;
|
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
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
generalized of_bool conversion
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
separated bit operations on type bit from generic syntactic bit operations
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
more lemmas on division
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 23:37:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 15:29:50 +0200 |
haftmann |
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
|
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
|
| Fri, 08 Mar 2013 13:21:06 +0100 |
kuncar |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file |
diff |
annotate
|
| Tue, 26 Feb 2013 20:09:25 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2012 17:18:55 +0200 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Fri, 18 May 2012 15:08:08 +0200 |
kuncar |
don't generate code in Word because it breaks the current code setup
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:32:30 +0200 |
huffman |
add code lemmas for word operations
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 23:57:44 +0200 |
kuncar |
setup_lifting: no_code switch and supoport for quotient theorems
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 19:16:13 +0200 |
kuncar |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 14:40:00 +0200 |
huffman |
remove now-unnecessary type annotations from lift_definition commands
|
file |
diff |
annotate
|