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