2008-05-08 wenzelm misc tuning;
2008-05-08 urbanc slight tuning of the 1st paragraph
2008-05-08 wenzelm unused;
2008-05-08 wenzelm converted HOL specific elements;
2008-05-08 wenzelm added rail setup for verblbrace, verbrbrace;
2008-05-08 urbanc added at_set_avoiding lemmas
2008-05-07 wenzelm removed obsolete conversion guide -- converted only section on tactics;
2008-05-07 wenzelm converted ZF specific elements;
2008-05-07 wenzelm enabled ThyOutput.source option by default;
2008-05-07 wenzelm output_entity: ignore ThyOutput.source option;
2008-05-07 wenzelm updated generated file;
2008-05-07 wenzelm converted HOLCF specific elements;
2008-05-07 wenzelm added logic-specific sessions;
2008-05-07 berghofe Updated.
2008-05-07 berghofe Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma
2008-05-07 berghofe Replaced instance declarations for sets by instance declarations for bool.
2008-05-07 berghofe Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm,
2008-05-07 berghofe Lookup and union operations on terms are now modulo eta conversion.
2008-05-07 berghofe Terms returned by decomp are now eta-contracted.
2008-05-07 berghofe Added function for computing instantiation for the subst rule, which is used
2008-05-07 berghofe eq_assumption now uses aeconv instead of aconv.
2008-05-07 berghofe - Removed function eta_contract_atom, which did not quite work
2008-05-07 berghofe Replaced Pattern.eta_contract_atom by Envir.eta_contract.
2008-05-07 berghofe Removed instantiation for set.
2008-05-07 berghofe Explicitely applied ext in proof of tnd.
2008-05-07 berghofe Deleted subset_antisym in a few proofs, because it is
2008-05-07 berghofe - Tuned imports
2008-05-07 berghofe Manually applied subset_antisym in proof of Compl_fixedpoint, because it is
2008-05-07 berghofe Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped
2008-05-07 berghofe Functions get_branching_types and get_arities now use fold instead of foldl/r.
2008-05-07 berghofe Temporarily disabled invocations of new code generator that do no
2008-05-07 berghofe Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"
2008-05-07 berghofe - Deleted arity proofs for set
2008-05-07 berghofe Replaced union_empty2 by Un_empty_right.
2008-05-07 berghofe Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
2008-05-07 berghofe Deleted instance "set :: ({heap, finite}) heap"
2008-05-07 berghofe - Declared subset_eq as code lemma
2008-05-07 berghofe Deleted instantiation "set :: (enum) enum"
2008-05-07 berghofe Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
2008-05-07 berghofe Rephrased calculational proofs to avoid problems with HO unification
2008-05-07 berghofe Rephrased forward proofs to avoid problems with HO unification
2008-05-07 berghofe Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification
2008-05-07 berghofe Locally deleted some definitions that were applied too eagerly because
2008-05-07 berghofe - Instantiated parts_insert_substD to avoid problems with HO unification
2008-05-07 berghofe Instantiated parts_insert_substD to avoid problems with HO unification
2008-05-07 berghofe Replaced blast by fast in proof of parts_singleton, since blast looped
2008-05-07 berghofe Adapted to encoding of sets as predicates
2008-05-07 berghofe Replaced forward proofs of existential statements by backward proofs
2008-05-07 berghofe Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
2008-05-07 berghofe - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
2008-05-07 berghofe Deleted instantiation "set :: (type) itself".
2008-05-07 berghofe - Function dec in Trancl_Tac must eta-contract relation before calling
2008-05-07 berghofe - Now uses Orderings as parent theory
2008-05-07 berghofe Deleted instance "set :: (type) power" and moved instance
2008-05-07 berghofe split_beta is now declared as monotonicity rule, to allow bounded
2008-05-07 berghofe - Added mem_def and predicate1I in some of the proofs
2008-05-07 berghofe - Now imports Code_Setup, rather than Set and Fun, since the theorems
2008-05-07 berghofe - Explicitely applied predicate1I in a few proofs, because it is no longer
2008-05-07 berghofe - Now imports Fun rather than Orderings
2008-05-07 berghofe Instantiated some rules to avoid problems with HO unification.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip