Wed, 01 Jan 2014 14:32:31 +0100 wenzelm updated keywords;
Wed, 01 Jan 2014 14:29:22 +0100 wenzelm clarified simplifier context;
Wed, 01 Jan 2014 13:24:23 +0100 wenzelm simplified settings for src/HOL/Tools/SMT;
Wed, 01 Jan 2014 12:57:26 +0100 wenzelm avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
Wed, 01 Jan 2014 15:55:11 +0100 haftmann dropped obsolete references to recdef
Wed, 01 Jan 2014 11:35:21 +0100 haftmann examples how to avoid the "code, code del" antipattern
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Wed, 01 Jan 2014 01:05:46 +0100 haftmann explicit distinction between empty code equations and no code equations, including convenient declaration attributes
Wed, 01 Jan 2014 01:05:30 +0100 haftmann tuned whitespace
Wed, 01 Jan 2014 01:05:30 +0100 haftmann more precise wording
Wed, 01 Jan 2014 01:05:30 +0100 haftmann uniform bookkeeping also in the case of deletion
Tue, 31 Dec 2013 22:18:31 +0100 haftmann more abstract declaration of code attributes
Tue, 31 Dec 2013 22:18:31 +0100 haftmann dropped unused material
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Tue, 31 Dec 2013 11:19:14 +0100 wenzelm made SML/NJ happy;
Mon, 30 Dec 2013 20:35:17 +0100 wenzelm added system option "jedit_print_mode";
Mon, 30 Dec 2013 12:58:13 +0100 wenzelm avoid hardwired /bin/bash (like canonical Isabelle shell scripts);
Mon, 30 Dec 2013 12:43:06 +0100 wenzelm tuned whitespace;
Sun, 29 Dec 2013 23:21:14 +0100 haftmann simplified
Sun, 29 Dec 2013 23:21:13 +0100 haftmann more compact representation of different situations for interpretation
Sun, 29 Dec 2013 23:21:12 +0100 haftmann more succint formulation of special case
Sun, 29 Dec 2013 23:21:11 +0100 haftmann tuned whitespace
Sat, 28 Dec 2013 21:06:26 +0100 haftmann move instantiation here from AFP/Native_Word
Sat, 28 Dec 2013 21:06:25 +0100 haftmann dropped junk
Sat, 28 Dec 2013 21:06:24 +0100 haftmann postpone dis"useful" lemmas
Sat, 28 Dec 2013 21:06:22 +0100 haftmann cleanup
Sat, 28 Dec 2013 17:51:54 +0100 haftmann prefix disambiguation
Fri, 27 Dec 2013 20:35:32 +0100 haftmann tuned proofs and declarations
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Thu, 26 Dec 2013 22:47:49 +0100 haftmann prefer ephemeral interpretation over interpretation in proof contexts;
Wed, 25 Dec 2013 22:35:29 +0100 haftmann self-contained formulation of subclass command, avoiding hard-wired Named_Target.init
Wed, 25 Dec 2013 22:35:28 +0100 haftmann ephemeral interpretation also formally works on theory level
Wed, 25 Dec 2013 17:39:07 +0100 haftmann abolished slightly odd global lattice interpretation for min/max
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Wed, 25 Dec 2013 17:39:06 +0100 haftmann explicit distributivity facts on min/max
Wed, 25 Dec 2013 15:52:25 +0100 haftmann postponed min/max lemmas until abstract lattice is available
Wed, 25 Dec 2013 15:52:25 +0100 haftmann tuned structure of min/max lemmas
Wed, 25 Dec 2013 15:52:25 +0100 haftmann prefer abstract simp rule
Wed, 25 Dec 2013 10:09:43 +0100 haftmann more lemmas on abstract lattices
Tue, 24 Dec 2013 11:24:16 +0100 haftmann tuning and augmentation of min/max lemmas;
Tue, 24 Dec 2013 11:24:14 +0100 haftmann more general induction rule;
Mon, 23 Dec 2013 20:45:33 +0100 haftmann convenient printing of polynomial values
Mon, 23 Dec 2013 18:37:51 +0100 haftmann prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
Mon, 23 Dec 2013 16:29:43 +0100 haftmann prefer Y_of_X over X_to_Y;
Mon, 23 Dec 2013 16:59:56 +0100 panny merge
Mon, 23 Dec 2013 15:30:31 +0100 panny prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
Mon, 23 Dec 2013 16:16:36 +0100 haftmann NEWS
Mon, 23 Dec 2013 14:24:22 +0100 haftmann dropped redundant lemma
Mon, 23 Dec 2013 14:24:21 +0100 haftmann syntactically tuned
Mon, 23 Dec 2013 14:24:20 +0100 haftmann prefer plain bool over dedicated type for binary digits
Mon, 23 Dec 2013 09:21:38 +0100 nipkow tuned
Sat, 21 Dec 2013 09:44:30 +0100 blanchet compile + reduce problem size by a notch
Sat, 21 Dec 2013 09:44:30 +0100 blanchet generate exhaust from nchotomy
Sat, 21 Dec 2013 09:44:29 +0100 blanchet made tactic work with theorems with multiple assumptions
Sat, 21 Dec 2013 09:44:28 +0100 blanchet renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
Wed, 18 Dec 2013 11:03:40 +0100 traytel express weak pullback property of bnfs only in terms of the relator
Fri, 20 Dec 2013 21:09:01 +0100 nipkow merged
Fri, 20 Dec 2013 21:08:48 +0100 nipkow tuned
Fri, 20 Dec 2013 20:36:38 +0100 blanchet reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Fri, 20 Dec 2013 16:22:10 +0100 blanchet tuning whitespace
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip