| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:57:01 +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 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
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
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
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
|
| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 14:24:20 +0100 |
haftmann |
prefer plain bool over dedicated type for binary digits
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
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 17:02:47 +0200 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
| Tue, 15 Jan 2013 17:28:46 +0100 |
wenzelm |
avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
|
file |
diff |
annotate
|
| Sat, 17 Nov 2012 17:55:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
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, 30 Jun 2010 16:28:13 +0200 |
haftmann |
use existing bit type from theory Bit
|
file |
diff |
annotate
|
| Wed, 20 Jan 2010 11:56:45 +0100 |
bulwahn |
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
|
file |
diff |
annotate
|
| Mon, 27 Apr 2009 11:27:19 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 15:09:12 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:42 +0200 |
berghofe |
Deleted subset_antisym in a few proofs, because it is
|
file |
diff |
annotate
|
| Fri, 04 Apr 2008 13:40:25 +0200 |
haftmann |
renamed app2 to map2
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 22:07:29 +0100 |
wenzelm |
avoid unclear fact references;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:01 +0100 |
wenzelm |
eliminated illegal schematic variables in where/of;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 21:09:21 +0200 |
huffman |
removed Word/Size.thy;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 16:55:46 +0200 |
huffman |
move bool list operations from WordBitwise to WordBoolList
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 02:04:30 +0200 |
huffman |
move bool list stuff from WordDefinition and WordArith to new WordBoolList theory
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 23:35:51 +0200 |
huffman |
remove redundant lemma int_number_of
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 23:00:17 +0200 |
huffman |
AC rules for bitwise logical operators no longer declared simp
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 19:51:01 +0200 |
huffman |
use overloaded bitwise operators at type int
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:11:09 +0200 |
huffman |
headers for document generation
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|