2007-04-10 huffman 2007-04-10 interpretation bounded_linear_of_real
2007-04-10 huffman 2007-04-10 removed unnecessary premise from power_le_imp_le_base
2007-04-10 krauss 2007-04-10 proper handling of morphisms
2007-04-10 krauss 2007-04-10 Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-04-10 wenzelm 2007-04-10 inline_antiq: no longer forces ML_Syntax.atomic;
2007-04-10 krauss 2007-04-10 removed dead code
2007-04-10 krauss 2007-04-10 tuned
2007-04-10 krauss 2007-04-10 added example for definitions in local contexts
2007-04-10 krauss 2007-04-10 removed obsolete workaround
2007-04-09 huffman 2007-04-09 generalized type of lemma setsum_product
2007-04-09 huffman 2007-04-09 new standard proofs of some LIMSEQ lemmas
2007-04-08 huffman 2007-04-08 rearranged sections
2007-04-08 huffman 2007-04-08 remove redundant lemmas
2007-04-07 krauss 2007-04-07 removed obsolete workarounds
2007-04-07 urbanc 2007-04-07 deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
2007-04-07 urbanc 2007-04-07 tuned slightly the previous commit
2007-04-07 narboux 2007-04-07 perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-04-06 huffman 2007-04-06 add new standard proofs for limits of sequences
2007-04-05 berghofe 2007-04-05 Replaced add_inductive_i by add_inductive_global.
2007-04-05 berghofe 2007-04-05 - Tried to make name_of_thm more robust against changes of the structure of proofs. - Now uses add_inductive_global rather than add_inductive_i for the definition of the realizability predicate.
2007-04-05 berghofe 2007-04-05 - Removed occurrences of ProofContext.export in add_ind_def that caused theorems to end up in the wrong context - Explicit parameters are now generalized in theorems returned by add_inductive(_i)
2007-04-05 wenzelm 2007-04-05 thy_deps: sort Context.thy_ord;
2007-04-05 wenzelm 2007-04-05 added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);
2007-04-04 wenzelm 2007-04-04 simplified thy_deps using Theory.ancestors_of (in order of creation);
2007-04-04 wenzelm 2007-04-04 renamed Variable.importT to importT_thms;
2007-04-04 wenzelm 2007-04-04 removed unused dep_graph;
2007-04-04 wenzelm 2007-04-04 theory: maintain ancestors in order of creation;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field; renamed Variable.importT to importT_thms;
2007-04-04 wenzelm 2007-04-04 rebind HOL.refl as refl (hidden by widen.refl);
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 narboux 2007-04-04 make fresh_guess fail if it does not solve the subgoal
2007-04-04 narboux 2007-04-04 add a few details in the Fst and Snd cases of unicity proof
2007-04-04 paulson 2007-04-04 find_first is just an alias
2007-04-04 wenzelm 2007-04-04 added print_mode (generic non-sense);
2007-04-04 wenzelm 2007-04-04 improved exception CTERM; removed obsolete sign_of/sign_of_thm;
2007-04-04 wenzelm 2007-04-04 removed unused info channel; renamed Output.has_mode to print_mode_active; cleaned-up Output functions;
2007-04-04 wenzelm 2007-04-04 added print_mode;
2007-04-04 wenzelm 2007-04-04 removed unused info channel;
2007-04-04 wenzelm 2007-04-04 renamed Output.has_mode to print_mode_active;
2007-04-04 wenzelm 2007-04-04 tuned comment;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions; removed unused info channel; moved print_mode to ROOT.ML (generic non-sense);
2007-04-04 wenzelm 2007-04-04 improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;
2007-04-04 wenzelm 2007-04-04 added scanwords from library.ML (for obsolete rename_tac);
2007-04-04 wenzelm 2007-04-04 removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
2007-04-04 wenzelm 2007-04-04 removed dead code;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions;
2007-04-04 wenzelm 2007-04-04 eliminated obsolete rename_tac;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-04-04 wenzelm 2007-04-04 ML antiquotes;
2007-04-03 wenzelm 2007-04-03 tuned comments;
2007-04-03 wenzelm 2007-04-03 fixed chr/explode;
2007-04-03 wenzelm 2007-04-03 avoid overloaded integer constants (accomodate Alice);
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2007-04-03 wenzelm 2007-04-03 signature: eqtype to accomodate Alice;
2007-04-03 wenzelm 2007-04-03 renamed comp to compose (avoid clash with Alice keywords);
2007-04-03 wenzelm 2007-04-03 renamed of_sort_derivation record fields (avoid clash with Alice keywords);
2007-04-03 wenzelm 2007-04-03 added ML-Systems/alice.ML;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-04-03 wenzelm 2007-04-03 ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);