2008-05-12 wenzelm 2008-05-12 misc tuning;
2008-05-10 wenzelm 2008-05-10 updated generated file;
2008-05-10 wenzelm 2008-05-10 fixed some labels;
2008-05-10 wenzelm 2008-05-10 avoid old macros from isar.sty;
2008-05-10 wenzelm 2008-05-10 misc reorganization;
2008-05-09 wenzelm 2008-05-09 added chapters for "Specifications" and "Proofs";
2008-05-09 wenzelm 2008-05-09 removed outdated comment;
2008-05-09 wenzelm 2008-05-09 updated generated file;
2008-05-09 wenzelm 2008-05-09 proper antiquotations for commands;
2008-05-09 wenzelm 2008-05-09 removed obsolete macros for Isar commands etc.; tuned;
2008-05-09 wenzelm 2008-05-09 replaced macros by antiquotations;
2008-05-09 wenzelm 2008-05-09 removed obsolete macros for Isar commands etc.;
2008-05-09 wenzelm 2008-05-09 added local copy of underscore.sty;
2008-05-08 wenzelm 2008-05-08 updated generated file;
2008-05-08 wenzelm 2008-05-08 replaced some latex macros by antiquotations;
2008-05-08 wenzelm 2008-05-08 removed obsolete macros; tuned;
2008-05-08 wenzelm 2008-05-08 removed obsolete math macros;
2008-05-08 wenzelm 2008-05-08 depend on style.sty;
2008-05-08 wenzelm 2008-05-08 updated generated file;
2008-05-08 wenzelm 2008-05-08 depend on ../../antiquote_setup.ML;
2008-05-08 wenzelm 2008-05-08 improved treatment of "_" thanks to underscore.sty;
2008-05-08 wenzelm 2008-05-08 clean_string: map "_" to "\\_" (best used with underscore.sty);
2008-05-08 wenzelm 2008-05-08 misc tuning;
2008-05-08 urbanc 2008-05-08 slight tuning of the 1st paragraph
2008-05-08 wenzelm 2008-05-08 unused;
2008-05-08 wenzelm 2008-05-08 converted HOL specific elements;
2008-05-08 wenzelm 2008-05-08 added rail setup for verblbrace, verbrbrace;
2008-05-08 urbanc 2008-05-08 added at_set_avoiding lemmas
2008-05-07 wenzelm 2008-05-07 removed obsolete conversion guide -- converted only section on tactics;
2008-05-07 wenzelm 2008-05-07 converted ZF specific elements;
2008-05-07 wenzelm 2008-05-07 enabled ThyOutput.source option by default;
2008-05-07 wenzelm 2008-05-07 output_entity: ignore ThyOutput.source option;
2008-05-07 wenzelm 2008-05-07 updated generated file;
2008-05-07 wenzelm 2008-05-07 converted HOLCF specific elements;
2008-05-07 wenzelm 2008-05-07 added logic-specific sessions;
2008-05-07 berghofe 2008-05-07 Updated.
2008-05-07 berghofe 2008-05-07 Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.
2008-05-07 berghofe 2008-05-07 Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.
2008-05-07 berghofe 2008-05-07 Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).
2008-05-07 berghofe 2008-05-07 Lookup and union operations on terms are now modulo eta conversion.
2008-05-07 berghofe 2008-05-07 Terms returned by decomp are now eta-contracted.
2008-05-07 berghofe 2008-05-07 Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.
2008-05-07 berghofe 2008-05-07 eq_assumption now uses aeconv instead of aconv.
2008-05-07 berghofe 2008-05-07 - Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv
2008-05-07 berghofe 2008-05-07 Replaced Pattern.eta_contract_atom by Envir.eta_contract.
2008-05-07 berghofe 2008-05-07 Removed instantiation for set.
2008-05-07 berghofe 2008-05-07 Explicitely applied ext in proof of tnd.
2008-05-07 berghofe 2008-05-07 Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.
2008-05-07 berghofe 2008-05-07 - Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.
2008-05-07 berghofe 2008-05-07 Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.
2008-05-07 berghofe 2008-05-07 Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.
2008-05-07 berghofe 2008-05-07 Functions get_branching_types and get_arities now use fold instead of foldl/r.
2008-05-07 berghofe 2008-05-07 Temporarily disabled invocations of new code generator that do no longer work due to the encoding of sets as predicates
2008-05-07 berghofe 2008-05-07 Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"
2008-05-07 berghofe 2008-05-07 - Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq
2008-05-07 berghofe 2008-05-07 Replaced union_empty2 by Un_empty_right.
2008-05-07 berghofe 2008-05-07 Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.
2008-05-07 berghofe 2008-05-07 Deleted instance "set :: ({heap, finite}) heap"
2008-05-07 berghofe 2008-05-07 - Declared subset_eq as code lemma - Deleted types_code declaration for sets
2008-05-07 berghofe 2008-05-07 Deleted instantiation "set :: (enum) enum"