| Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 13:29:38 +0200 |
haftmann |
more coherent naming of syntax data structures
|
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 12:57:55 +0200 |
wenzelm |
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 12:19:49 +0200 |
haftmann |
prevent line breaks after Scala symbolic operators
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 21:04:22 +0200 |
wenzelm |
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 12:12:32 +0200 |
haftmann |
tuned; added pretty numerals for code generation
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:13:14 +0200 |
haftmann |
avoid export_code ... file -
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
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
|
| Wed, 03 Mar 2010 00:32:14 +0100 |
wenzelm |
adapted to authentic syntax -- actual types are verbatim;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:17:33 +0100 |
wenzelm |
explicit @{type_syntax} markup;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:19:58 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:17:35 +0100 |
wenzelm |
recovered from 7a1f597f454e, simplified imports;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 08:14:23 +0100 |
haftmann |
adjusted import to changed HOL theory graph
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Thu, 30 Apr 2009 12:16:35 -0700 |
huffman |
used named theorems for declaring numeral simps
|
file |
diff |
annotate
|
| Thu, 30 Apr 2009 11:14:04 -0700 |
huffman |
clean up unsigned numeral proofs
|
file |
diff |
annotate
|
| Thu, 30 Apr 2009 07:33:40 -0700 |
huffman |
detect error cases in mk_num, dest_num
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 20:33:52 -0700 |
huffman |
add semiring_assoc_fold simproc for unsigned numerals
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:57:16 -0700 |
huffman |
reorient simproc for unsigned numerals
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 15:14:31 -0700 |
huffman |
add more lemmas for signed comparisons
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 08:07:52 -0800 |
huffman |
add more ordering lemmas
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 20:45:23 -0800 |
huffman |
add lemmas for exponentiation
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 19:35:52 -0800 |
huffman |
tune section headings; add square function
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:42:45 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:42:15 -0800 |
huffman |
rearrange subsections
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:14:36 -0800 |
huffman |
remove instances num::semiring and num::linorder
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:08:21 -0800 |
huffman |
datatype num = One | Dig0 num | Dig1 num
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 12:53:59 -0800 |
huffman |
replace 1::num with One; remove monoid_mult instance
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 19:53:20 -0800 |
huffman |
replace dec with double-and-decrement function
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 13:38:10 +0100 |
haftmann |
tuned texts
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 09:09:51 +0200 |
haftmann |
op = vs. eq
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|