2005-11-02 wenzelm 2005-11-02 added Isar.state/exn;
2005-11-02 wenzelm 2005-11-02 Isar.loop;
2005-11-02 wenzelm 2005-11-02 moved consts declarations to consts.ML;
2005-11-02 wenzelm 2005-11-02 Consts.dest;
2005-11-02 wenzelm 2005-11-02 Polymorphic constants.
2005-11-02 wenzelm 2005-11-02 added consts.ML;
2005-11-02 wenzelm 2005-11-02 fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
2005-11-02 wenzelm 2005-11-02 dist_eqI: the_context();
2005-11-02 wenzelm 2005-11-02 Sign.const_monomorphic;
2005-11-02 wenzelm 2005-11-02 Logic.nth_prem;
2005-11-02 urbanc 2005-11-02 added the collection of lemmas "supp_at"
2005-11-01 urbanc 2005-11-01 some minor tweaks in some proofs (nothing extraordinary)
2005-11-01 urbanc 2005-11-01 tunings of some comments (nothing serious)
2005-10-31 haftmann 2005-10-31 nth_*, fold_index refined
2005-10-31 haftmann 2005-10-31 fold_index replacing foldln
2005-10-31 nipkow 2005-10-31 A few new lemmas
2005-10-30 urbanc 2005-10-30 tuned my last commit
2005-10-30 urbanc 2005-10-30 simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML
2005-10-29 urbanc 2005-10-29 Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.
2005-10-29 urbanc 2005-10-29 1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 wenzelm 2005-10-28 lthms_containing: not o valid_thms;
2005-10-28 wenzelm 2005-10-28 added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28 wenzelm 2005-10-28 added fact method; accomodate simplified Thm.lift_rule;
2005-10-28 wenzelm 2005-10-28 tuned ProofContext.export interfaces;
2005-10-28 wenzelm 2005-10-28 syntax for literal facts;
2005-10-28 wenzelm 2005-10-28 removed try_dest_Goal, use Logic.unprotect;
2005-10-28 wenzelm 2005-10-28 added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule; tuned;
2005-10-28 wenzelm 2005-10-28 export cong_modifiers, simp_modifiers';
2005-10-28 wenzelm 2005-10-28 certify_term: tuned monomorphic consts;
2005-10-28 wenzelm 2005-10-28 datatype thmref: added Fact; renamed Goal constant to prop;
2005-10-28 wenzelm 2005-10-28 Logic.lift_all;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;
2005-10-28 wenzelm 2005-10-28 renamed Goal.norm_hhf_rule to Goal.norm_hhf;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all;
2005-10-28 wenzelm 2005-10-28 added add_local/add_global; index props (for add_local only); added could_unify;
2005-10-28 wenzelm 2005-10-28 added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule;
2005-10-28 wenzelm 2005-10-28 Logic.unprotect;
2005-10-28 wenzelm 2005-10-28 literal facts;
2005-10-28 wenzelm 2005-10-28 * Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 webertj 2005-10-28 unnecessary imports removed
2005-10-28 urbanc 2005-10-28 fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
2005-10-28 berghofe 2005-10-28 Implemented proof of weak induction theorem.
2005-10-28 berghofe 2005-10-28 Added "deepen" method.
2005-10-28 haftmann 2005-10-28 circumvented smlnj value restriction
2005-10-28 haftmann 2005-10-28 added extraction interface for code generator
2005-10-28 urbanc 2005-10-28 Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28 berghofe 2005-10-28 Removed legacy prove_goalw_cterm command.
2005-10-28 paulson 2005-10-28 got rid of obsolete prove_goalw_cterm
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-28 haftmann 2005-10-28 removed obfuscating PStrStrTab
2005-10-28 haftmann 2005-10-28 reachable - abandoned foldl_map in favor of fold_map
2005-10-28 mengj 2005-10-28 Added Tools/res_hol_clause.ML