2012-01-14 wenzelm 2012-01-14 tuned comment;
2012-01-14 wenzelm 2012-01-14 paranoia null check -- prevent spurious crash of jedit token markup;
2012-01-14 wenzelm 2012-01-14 tuned comments;
2012-01-14 wenzelm 2012-01-14 tuned signature;
2012-01-14 wenzelm 2012-01-14 clarified partial restrict operation;
2012-01-14 wenzelm 2012-01-14 tuned proofs;
2012-01-14 wenzelm 2012-01-14 ignore empty gfx_range; tuned;
2012-01-14 wenzelm 2012-01-14 tuned signature;
2012-01-13 nipkow 2012-01-13 tuned
2012-01-13 wenzelm 2012-01-13 handle specific exception, not arbitrary ones (including Interrupt);
2012-01-13 wenzelm 2012-01-13 eliminated dead code;
2012-01-12 wenzelm 2012-01-12 more modest settings for lxbroy10 -- might actually perform better;
2012-01-12 wenzelm 2012-01-12 tuned;
2012-01-12 wenzelm 2012-01-12 improved select_markup: include filtering of defined results;
2012-01-12 wenzelm 2012-01-12 tuned text_color: cumulate with explicit default color;
2012-01-12 wenzelm 2012-01-12 added cat_lines convenience;
2012-01-12 wenzelm 2012-01-12 tuned;
2012-01-12 wenzelm 2012-01-12 clarified mkString: no extra line-breaks for XML.Body;
2012-01-12 bulwahn 2012-01-12 adding exhaustive instances for type constructor set
2012-01-12 berghofe 2012-01-12 Updated generated file
2012-01-12 berghofe 2012-01-12 Added inf_Int_eq to pred_set_conv database as well
2012-01-11 wenzelm 2012-01-11 more conventional eval_tac vs. method_setup "eval"; clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;
2012-01-11 wenzelm 2012-01-11 updated generated file -- change of printed case syntax probably due to f805747f8571;
2012-01-11 wenzelm 2012-01-11 actually try to preserve names given by user (cf. 463b594e186a);
2012-01-11 wenzelm 2012-01-11 updated example -- List.foldl is no longer defined via primrec;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;
2012-01-11 wenzelm 2012-01-11 refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;
2012-01-11 wenzelm 2012-01-11 more robust ISABELLE_HOME_USER for repository versions -- some versions of Emacs interpret foo//bar as /bar even on the command-line (unlike regular POSIX semantics);
2012-01-11 berghofe 2012-01-11 merged
2012-01-11 berghofe 2012-01-11 Removed strange hack introduced in b27e93132603, since equivariance is working again
2012-01-10 berghofe 2012-01-10 Replaced perm_set_eq by perm_set_def
2012-01-10 berghofe 2012-01-10 Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete pt_insert_eqvt, pt_set_eqvt, and perm_set_eq
2012-01-10 berghofe 2012-01-10 Reverted several lemmas involving sets to the state before the removal of the set type.
2012-01-10 wenzelm 2012-01-10 clarified Isabelle_Rendering vs. physical painting; discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;
2012-01-10 berghofe 2012-01-10 pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
2012-01-10 berghofe 2012-01-10 pred_subset/equals_eq are now standard pred_set_conv rules
2012-01-10 berghofe 2012-01-10 Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
2012-01-10 huffman 2012-01-10 merged
2012-01-10 huffman 2012-01-10 add simp rules for set_bit and msb applied to 0 and 1
2012-01-10 huffman 2012-01-10 add simp rule test_bit_1
2012-01-10 bulwahn 2012-01-10 proper hiding of facts and constants in AList_Impl and AList theory
2012-01-10 bulwahn 2012-01-10 NEWS
2012-01-10 bulwahn 2012-01-10 adding quickcheck examples with multisets
2012-01-10 bulwahn 2012-01-10 improving code generation for multisets; adding exhaustive quickcheck generators for multisets
2012-01-10 bulwahn 2012-01-10 adding theory association lists with invariant
2012-01-09 wenzelm 2012-01-09 command status color via regular markup;
2012-01-09 wenzelm 2012-01-09 proper cumulation of bulk arguments;
2012-01-09 wenzelm 2012-01-09 tuned;
2012-01-09 blanchet 2012-01-09 merge
2012-01-09 blanchet 2012-01-09 revert unintended "sledgehammer" call
2012-01-09 wenzelm 2012-01-09 prefer antiquotations;
2012-01-09 wenzelm 2012-01-09 misc tuning and reformatting;
2012-01-09 wenzelm 2012-01-09 updated generated file;
2012-01-09 nipkow 2012-01-09 Added termination to IMP Abs_Int
2012-01-09 nipkow 2012-01-09 added lemmas
2012-01-07 haftmann 2012-01-07 massaging of code setup for sets
2012-01-07 haftmann 2012-01-07 dropped theory More_Set
2012-01-07 haftmann 2012-01-07 use Inf/Sup_bool_def/apply as code equations
2012-01-07 nipkow 2012-01-07 tuned
2012-01-07 wenzelm 2012-01-07 accumulate status as regular markup for command range; tuned signature;