| Thu, 18 Jun 2020 09:07:29 +0000 |
haftmann |
eliminated warnings
|
file |
diff |
annotate
|
| Sat, 09 May 2020 17:20:04 +0000 |
haftmann |
modernized notation for bit operations
|
file |
diff |
annotate
|
| Fri, 22 Nov 2019 09:25:01 +0000 |
haftmann |
proper prefix syntax
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 18:41:33 +0000 |
haftmann |
moved quickcheck setup to distribution
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 18:41:31 +0000 |
haftmann |
moved generic instance to distribution
|
file |
diff |
annotate
|
| Tue, 24 Sep 2019 12:56:10 +0100 |
paulson |
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
clear separation of types for bits (False / True) and Z2 (0 / 1)
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
consolidated map2 clones
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
separate type class for bit comprehension
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 09:33:55 +0000 |
haftmann |
no need to maintain two separate type classes
|
file |
diff |
annotate
|
| Mon, 22 Apr 2019 06:28:17 +0000 |
haftmann |
clarified structure of theories
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:21 +0000 |
haftmann |
avoid separate type class for mere definitional extension
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 18:02:20 +0000 |
haftmann |
tuned name
|
file |
diff |
annotate
|
| Sat, 20 Apr 2019 13:44:16 +0000 |
haftmann |
clarified notation
|
file |
diff |
annotate
|
| Thu, 18 Apr 2019 06:06:54 +0000 |
haftmann |
incorporated various material from the AFP into the distribution
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:20 +0000 |
haftmann |
eliminated type class
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:18 +0000 |
haftmann |
tuned theory names
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:05 +0000 |
haftmann |
prefer one theory for misc material
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:03 +0000 |
haftmann |
moved instance to appropriate place
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Sat, 12 May 2018 22:20:46 +0200 |
haftmann |
removed some non-essential rules
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 03 Dec 2017 19:09:42 +0100 |
wenzelm |
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Tue, 24 Oct 2017 18:48:21 +0200 |
immler |
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 23:12:16 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2017 21:44:41 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sun, 19 Mar 2017 18:28:32 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2017 19:33:34 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 20:59:51 +0200 |
wenzelm |
clarified session;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| 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
|