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;
2008-03-17 wenzelm 2008-03-17 proper naming of weak_ref_map2ref_map;
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts; proper ML antiquotations;
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-03-17 wenzelm 2008-03-17 added Compl_Collect;
2008-03-17 wenzelm 2008-03-17 proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;
2008-03-17 wenzelm 2008-03-17 renamed K3_imp_Gets variant to K3_imp_Gets_evs;
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-03-17 wenzelm 2008-03-17 closeup: recover original order of free variables!
2008-03-17 nipkow 2008-03-17 reorganization
2008-03-17 nipkow 2008-03-17 added lemmas
2008-03-17 huffman 2008-03-17 remove unneeded constant mod_alt
2008-03-17 nipkow 2008-03-17 More defns and thms
2008-03-17 kleing 2008-03-17 fixed broken bintrunc lemma