Mon, 06 Jan 2014 17:33:23 +0100 wenzelm tuned comments;
Mon, 06 Jan 2014 19:55:01 +0100 haftmann dropped legacy
Mon, 06 Jan 2014 09:31:21 +0100 haftmann order and graph for code symbols
Mon, 06 Jan 2014 09:31:19 +0100 haftmann special treatment of ==> and == solely as constants
Mon, 06 Jan 2014 09:31:18 +0100 haftmann uniform orientation of instances as (type constructor, type class)
Sun, 05 Jan 2014 18:59:29 +0100 nipkow minimized class dependency, updated references
Fri, 03 Jan 2014 22:04:44 +0100 haftmann proper context for simplifier invocations in code generation stack
Fri, 03 Jan 2014 21:52:00 +0100 haftmann spelling
Fri, 03 Jan 2014 14:38:13 +0100 blanchet proper name generation to avoid clash with 'P' in user specification
Fri, 03 Jan 2014 14:14:16 +0100 blanchet more SML-ish (less Haskell-ish) naming convention
Fri, 03 Jan 2014 14:04:37 +0100 blanchet strengthened tactic
Fri, 03 Jan 2014 13:55:34 +0100 blanchet refactoring
Fri, 03 Jan 2014 11:26:44 +0100 blanchet instantiate schematics as projections to avoid HOU trouble
Fri, 03 Jan 2014 10:48:48 +0100 blanchet tuning
Thu, 02 Jan 2014 23:44:31 +0100 blanchet avoid schematic variable in goal, which sometimes gets instantiated by tactic
Thu, 02 Jan 2014 23:07:49 +0100 blanchet generalized tactic to the case of several assumptions per equation
Thu, 02 Jan 2014 22:23:00 +0100 blanchet made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)
Thu, 02 Jan 2014 21:35:21 +0100 blanchet made tactic more robust
Thu, 02 Jan 2014 20:51:09 +0100 blanchet made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip