Thu, 02 Jan 2014 20:25:40 +0100 blanchet simplified code
Thu, 02 Jan 2014 20:10:08 +0100 blanchet prevent tactic from getting out of sync and wrongly attack next subgoal
Thu, 02 Jan 2014 19:07:36 +0100 blanchet removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
Thu, 02 Jan 2014 09:50:22 +0100 blanchet consider code as exhaustive
Thu, 02 Jan 2014 09:50:22 +0100 blanchet proper handling of corner case, take 2
Thu, 02 Jan 2014 09:50:22 +0100 blanchet robustness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet properly synchronize parallel lists
Thu, 02 Jan 2014 09:50:22 +0100 blanchet graceful handling of one-constructor case
Thu, 02 Jan 2014 09:50:22 +0100 blanchet gracefully handle single-equation case, where 'nchotomy' is 'True'
Thu, 02 Jan 2014 09:50:22 +0100 blanchet made tactic handle gracefully the case of missing constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet removed 'nchotomy' property
Thu, 02 Jan 2014 09:50:22 +0100 blanchet don't generate any proof obligation for implicit (de facto) exclusiveness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet detect syntactic exhaustiveness
Thu, 02 Jan 2014 09:50:22 +0100 blanchet internally allow different values for 'exhaustive' for different constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet internally allow different values for 'sequential' for different constructors
Thu, 02 Jan 2014 09:50:22 +0100 blanchet use same name for feature internally as in user interface, to facilitate grepping
Thu, 02 Jan 2014 09:50:22 +0100 blanchet generate 'disc_iff' property in 'primcorec'
Thu, 02 Jan 2014 09:50:22 +0100 blanchet added tactic to prove 'disc_iff' properties in 'primcorec'
Wed, 01 Jan 2014 21:23:32 +0100 wenzelm merged
Wed, 01 Jan 2014 20:14:47 +0100 wenzelm clarified blast after change of SELECT_GOAL in 210bca64b894: do not smash flex-flex pairs of overall goal state (in analogy to maxidx) -- NB: Isar goal structure serves as natural boundary, e.g. in "by blast";
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip