2008-03-20 wenzelm 2008-03-20 added pos_of_ref;
2008-03-20 wenzelm 2008-03-20 fixed proof;
2008-03-20 berghofe 2008-03-20 Equivariance prover now uses permutation simprocs as well.
2008-03-20 wenzelm 2008-03-20 export add/del_thm;
2008-03-20 wenzelm 2008-03-20 added print_properties, print_position;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 haftmann 2008-03-20 tuned proofs
2008-03-20 haftmann 2008-03-20 more antiquotations
2008-03-20 haftmann 2008-03-20 Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
2008-03-20 haftmann 2008-03-20 added forward composition
2008-03-20 haftmann 2008-03-20 Product_Type.apfst and Product_Type.apsnd
2008-03-20 haftmann 2008-03-20 Theory Product_Type; fixed typos
2008-03-20 haftmann 2008-03-20 rearranged
2008-03-20 haftmann 2008-03-20 (continued)
2008-03-20 haftmann 2008-03-20 tuned
2008-03-20 haftmann 2008-03-20 tuned import
2008-03-20 haftmann 2008-03-20 adjusted authorship
2008-03-20 haftmann 2008-03-20 tuned proof
2008-03-20 haftmann 2008-03-20 added theory Library/Enum.thy
2008-03-20 haftmann 2008-03-20 tuned proofs
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument; renamed former get_thm to get_fact_single, and get_thms to get_fact;
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument; renamed former get_thms(_silent) to get_fact(_silent);
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2008-03-19 wenzelm 2008-03-19 avoid Auto_tac;
2008-03-19 wenzelm 2008-03-19 more antiquotations; eliminated change_claset/simpset;
2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup; renamed local dynamic_thm(s) to goal_thm(s);
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_not_sym, Nat.less_asym; renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_irrefl;
2008-03-19 paulson 2008-03-19 Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.
2008-03-19 wenzelm 2008-03-19 system: writeln output, if available;
2008-03-19 haftmann 2008-03-19 error tuning
2008-03-19 haftmann 2008-03-19 moved typ_of_inst to Type.typ_of_sort
2008-03-19 haftmann 2008-03-19 instantiation less liberal with dangling constraints
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2008-03-19 haftmann 2008-03-19 Type.lookup now curried; typ_of_sort
2008-03-19 haftmann 2008-03-19 new class error case NoSubsort
2008-03-19 haftmann 2008-03-19 quickcheck with term reconstruction
2008-03-19 haftmann 2008-03-19 whitespace tuning
2008-03-18 wenzelm 2008-03-18 theory loader: discontinued *attached* ML scripts;
2008-03-18 wenzelm 2008-03-18 converted legacy ML scripts;
2008-03-18 wenzelm 2008-03-18 valid_thms: get_thms_silent;
2008-03-18 wenzelm 2008-03-18 removed check_lookup; added get_thms_silent;
2008-03-18 wenzelm 2008-03-18 added ckeck_lookup flag (default false), which controls sanity check of thm lookup;
2008-03-18 wenzelm 2008-03-18 updated generated files;
2008-03-18 wenzelm 2008-03-18 tuned proof;
2008-03-18 wenzelm 2008-03-18 removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
2008-03-18 wenzelm 2008-03-18 removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy); renamed less_imp_le to less_imp_le_nat;
2008-03-18 wenzelm 2008-03-18 avoid rebinding of existing facts;
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts; removed duplicate lemmas;
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-03-17 wenzelm 2008-03-17 only one version of group.rcos_self;
2008-03-17 wenzelm 2008-03-17 Facts.add_local;
2008-03-17 wenzelm 2008-03-17 Facts.add_global;
2008-03-17 wenzelm 2008-03-17 replaced generic add by add_local/add_global; add_global: report/ignore duplicate bindings;