2002-07-28 wenzelm 2002-07-28 tuned document;
2002-07-27 wenzelm 2002-07-27 make SML/NJ happy;
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-26 wenzelm 2002-07-26 tuned;
2002-07-25 paulson 2002-07-25 More lemmas, working towards relativization of "satisfies"
2002-07-25 paulson 2002-07-25 Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale.
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-24 wenzelm 2002-07-24 removed unused locale_facts(_i); simplified locale predicates: only one level for zero imports; tuned;
2002-07-24 wenzelm 2002-07-24 tuned;
2002-07-24 paulson 2002-07-24 tweaks, aiming towards relativization of "satisfies"
2002-07-24 berghofe 2002-07-24 Tuned type constraint of function merge_rules to make smlnj happy.
2002-07-24 wenzelm 2002-07-24 AC18: meta-level predicate via locale;
2002-07-24 wenzelm 2002-07-24 tuned view;
2002-07-24 wenzelm 2002-07-24 removed attribute "norm_hhf";
2002-07-24 wenzelm 2002-07-24 adapted fact names;
2002-07-24 wenzelm 2002-07-24 predicate defs via locales;
2002-07-24 wenzelm 2002-07-24 locales: predicate defs;
2002-07-24 wenzelm 2002-07-24 * Pure: locale specifications now produce predicate definitions;
2002-07-23 paulson 2002-07-23 Relativization and Separation for the function "nth"
2002-07-22 berghofe 2002-07-22 Added "nocite" to avoid BibTeX error when proofs are switched off.
2002-07-21 berghofe 2002-07-21 Added program extraction keywords.
2002-07-21 berghofe 2002-07-21 Document for program extraction in HOL.
2002-07-21 berghofe 2002-07-21 Examples for program extraction in HOL.
2002-07-21 berghofe 2002-07-21 Rules for rewriting HOL proofs.
2002-07-21 berghofe 2002-07-21 Added theory for setting up program extraction.
2002-07-21 berghofe 2002-07-21 Added program extraction module.
2002-07-19 wenzelm 2002-07-19 *** empty log message ***
2002-07-19 wenzelm 2002-07-19 accomodate cumulative locale predicates;
2002-07-19 wenzelm 2002-07-19 support locale ``views'' (for cumulative predicates);
2002-07-19 paulson 2002-07-19 Towards relativization and absoluteness of formula_rec
2002-07-19 paulson 2002-07-19 Absoluteness of the function "nth"
2002-07-19 paulson 2002-07-19 A couple of new theorems for Constructible
2002-07-18 paulson 2002-07-18 absoluteness for "formula" and "eclose"
2002-07-18 wenzelm 2002-07-18 define cumulative predicate view; tuned;
2002-07-18 wenzelm 2002-07-18 adapted add_locale;
2002-07-18 wenzelm 2002-07-18 adapted locale syntax;
2002-07-18 wenzelm 2002-07-18 fixed inform_file_retracted: remove_thy;
2002-07-18 wenzelm 2002-07-18 ACe_axioms;
2002-07-18 wenzelm 2002-07-18 added satisfy_hyps;
2002-07-18 wenzelm 2002-07-18 quantify LC (conflict with const name of HOL);
2002-07-18 paulson 2002-07-18 new theorems to support Constructible proofs
2002-07-17 paulson 2002-07-17 Formulas (and lists) in M (and L!)
2002-07-17 paulson 2002-07-17 Expressing Lset and L without using length and arity; simplifies Separation proofs
2002-07-16 schirmer 2002-07-16 Added conditional and (&&) and or (||).
2002-07-16 wenzelm 2002-07-16 adapted locales;
2002-07-16 wenzelm 2002-07-16 adapted locales;
2002-07-16 wenzelm 2002-07-16 tuned;
2002-07-16 wenzelm 2002-07-16 adapted locales; tuned;
2002-07-16 wenzelm 2002-07-16 rearranged to work without proof contexts;
2002-07-16 wenzelm 2002-07-16 export_standard supercedes export_single;
2002-07-16 wenzelm 2002-07-16 export map_context; removed internal interface put_data;
2002-07-16 wenzelm 2002-07-16 assert_propT;
2002-07-16 wenzelm 2002-07-16 proper predicate definitions of locale body;
2002-07-16 wenzelm 2002-07-16 add_locale: adapted args;
2002-07-16 wenzelm 2002-07-16 locale: optional predicate name, or "open";
2002-07-16 wenzelm 2002-07-16 module now right after ProofContext (for locales);
2002-07-16 wenzelm 2002-07-16 avoid "_st" versions of proof data;
2002-07-16 wenzelm 2002-07-16 context rules;
2002-07-16 wenzelm 2002-07-16 tuned order of modules;
2002-07-16 wenzelm 2002-07-16 added equal_elim_rule1;