Sat, 16 Jan 2010 17:15:27 +0100 haftmann explicit CONST in translations
Sat, 16 Jan 2010 17:15:27 +0100 haftmann modernized syntax
Wed, 20 Jan 2010 11:54:19 +0100 blanchet fix issues with previous Nitpick change
Wed, 20 Jan 2010 10:38:19 +0100 blanchet merged
Wed, 20 Jan 2010 10:38:06 +0100 blanchet some work on Nitpick's support for quotient types;
Thu, 14 Jan 2010 17:06:35 +0100 blanchet removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
Tue, 19 Jan 2010 17:53:11 +0100 hoelzl Added transpose_rectangle, when the input list is rectangular.
Tue, 19 Jan 2010 16:52:01 +0100 hoelzl Add transpose to the List-theory.
Tue, 02 Feb 2010 21:37:27 +0100 wenzelm some examples for basic context operations;
Tue, 02 Feb 2010 13:22:36 +0100 wenzelm minimal tuning of this slightly dated material;
Tue, 02 Feb 2010 13:11:04 +0100 wenzelm added Subgoal.FOCUS;
Tue, 02 Feb 2010 12:37:57 +0100 wenzelm misc tuning and clarification;
Tue, 02 Feb 2010 11:47:49 +0100 wenzelm moved examples to proper place;
Mon, 01 Feb 2010 22:46:12 +0100 wenzelm more details on long names, binding/naming, name space;
Sun, 31 Jan 2010 22:08:25 +0100 wenzelm Variable.names_of;
Sun, 31 Jan 2010 21:40:44 +0100 wenzelm more details on Isabelle symbols;
Fri, 29 Jan 2010 23:59:03 +0100 wenzelm theory data example;
Fri, 29 Jan 2010 23:57:57 +0100 wenzelm basic setup for ML examples: tag "mlex";
Thu, 28 Jan 2010 22:39:48 +0100 wenzelm tuned signature;
Thu, 28 Jan 2010 22:38:11 +0100 wenzelm formal markup of type aliases;
Thu, 28 Jan 2010 22:19:27 +0100 wenzelm make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
Sat, 16 Jan 2010 21:14:15 +0100 wenzelm Netbeans Library "Scala-compiler";
Fri, 15 Jan 2010 19:14:51 +0100 berghofe union is an abbreviation for sup.
Fri, 15 Jan 2010 14:43:00 +0100 berghofe merged
Fri, 15 Jan 2010 13:37:41 +0100 berghofe Eliminated is_open option of Rule_Cases.make_nested/make_common;
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Sun, 10 Jan 2010 18:41:07 +0100 berghofe Adapted to changes in setup of induct method.
Sun, 10 Jan 2010 18:39:50 +0100 berghofe Expand proofs of induct_atomize'/rulify'.
Sun, 10 Jan 2010 18:37:37 +0100 berghofe Changed case names of converse_rtranclp_induct.
Sun, 10 Jan 2010 18:11:00 +0100 berghofe Injectivity / distinctness theorems are now used to simplify induction rules.
Sun, 10 Jan 2010 18:09:11 +0100 berghofe same_append_eq / append_same_eq are now used for simplifying induction rules.
Sun, 10 Jan 2010 18:06:30 +0100 berghofe Tuned some proofs; nicer case names for some of the induction / cases rules.
Sun, 10 Jan 2010 18:03:20 +0100 berghofe Added setup for simplification of equality constraints in induction rules.
Sun, 10 Jan 2010 18:01:04 +0100 berghofe Added infrastructure for simplifying equality constraints.
Fri, 15 Jan 2010 08:27:21 +0100 haftmann spurious proof failure
Thu, 14 Jan 2010 18:44:22 +0100 haftmann merged
Thu, 14 Jan 2010 18:42:15 +0100 haftmann merged
Thu, 14 Jan 2010 17:54:55 +0100 haftmann dropped unused binding
Thu, 14 Jan 2010 17:54:54 +0100 haftmann dedicated conversions to and from Int
Thu, 14 Jan 2010 17:47:39 +0100 haftmann printing of cases
Thu, 14 Jan 2010 17:47:39 +0100 haftmann tuned for products vs. tupled functions
Thu, 14 Jan 2010 17:47:39 +0100 haftmann added Scala setup
Thu, 14 Jan 2010 17:47:38 +0100 haftmann allow individual printing of numerals during code serialization
Thu, 14 Jan 2010 15:06:38 +0100 blanchet reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
Thu, 14 Jan 2010 09:18:08 +0100 haftmann adjusted to changes in code equation administration
Wed, 13 Jan 2010 12:20:37 +0100 haftmann explicit abstract type of code certificates
Wed, 13 Jan 2010 10:18:45 +0100 haftmann corrected error messages; tuned
Wed, 13 Jan 2010 10:18:45 +0100 haftmann function transformer preprocessor applies to both code generators
Wed, 13 Jan 2010 09:13:30 +0100 haftmann merged
Tue, 12 Jan 2010 16:27:42 +0100 haftmann code certificates as integral part of code generation
Wed, 13 Jan 2010 09:02:47 +0100 haftmann import of antiquote_setup not necessary
Wed, 13 Jan 2010 08:56:25 +0100 haftmann merged
Wed, 13 Jan 2010 08:56:16 +0100 haftmann being more accurate wrt. list syntax
Wed, 13 Jan 2010 08:56:16 +0100 haftmann deactivate pretty code test for Scala -- no proper setup yet
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Wed, 13 Jan 2010 00:08:56 +0100 wenzelm added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
Tue, 12 Jan 2010 22:53:18 +0100 wenzelm merged
Tue, 12 Jan 2010 16:55:59 +0000 paulson Parsing errors during proof reconstruction now give rise to an intelligible error message.
Tue, 12 Jan 2010 22:23:29 +0100 wenzelm rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
Tue, 12 Jan 2010 17:06:36 +0100 wenzelm tuned initial properties/perspective;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip