2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-20 krauss 2006-06-20 Fixed another variable order bug...
2006-06-20 haftmann 2006-06-20 switched to open locales for classes
2006-06-20 haftmann 2006-06-20 switched to open locales for classes
2006-06-19 wenzelm 2006-06-19 refrain from reforming TFL -- back to previous revision;
2006-06-19 wenzelm 2006-06-19 added declare_thm, thm_context; added trade(T);
2006-06-19 wenzelm 2006-06-19 eliminated freeze/varify in favour of Variable.import/export/trade;
2006-06-19 webertj 2006-06-19 world map updated
2006-06-19 webertj 2006-06-19 world map updated
2006-06-19 krauss 2006-06-19 Fixed name clash. Function-goals are now fully quantified. Avoiding large meta-conjunctions when setting up the goal. Cleanup.
2006-06-19 webertj 2006-06-19 world map updated
2006-06-19 wenzelm 2006-06-19 matchers: try pattern_matchers only *after* general matching (The pattern version is not a faithful approximation because it falls back on first-order matching!);
2006-06-17 wenzelm 2006-06-17 ProofContext.exports: simultaneous facts;
2006-06-17 wenzelm 2006-06-17 moved internal/skolem to term.ML;
2006-06-17 wenzelm 2006-06-17 mutual_rule: proper context;
2006-06-17 wenzelm 2006-06-17 export: simultaneous facts, refer to Variable.export; Term.internal/skolem;
2006-06-17 wenzelm 2006-06-17 ProofContext.exports: simultaneous facts; Variable.exportT_terms;
2006-06-17 wenzelm 2006-06-17 Variable.importT_inst; Term.internal;
2006-06-17 wenzelm 2006-06-17 standard: simultaneous facts;
2006-06-17 wenzelm 2006-06-17 added singleton;
2006-06-17 wenzelm 2006-06-17 major reworking of export functionality -- based on Term/Thm.generalize; tuned interfaces;
2006-06-17 wenzelm 2006-06-17 added generalize rule; added maxidx_thm;
2006-06-17 wenzelm 2006-06-17 added exists_subtype; added internal/skolem (from Syntax/lexicon.ML); added generalize(T);
2006-06-17 wenzelm 2006-06-17 added generalize rule;
2006-06-17 wenzelm 2006-06-17 Term.skolem;
2006-06-17 wenzelm 2006-06-17 Term.internal;
2006-06-17 wenzelm 2006-06-17 ProofContext.export: singleton;
2006-06-17 wenzelm 2006-06-17 RuleCases.mutual_rule: ctxt; ProofContext.exports: simultaneous facts;
2006-06-17 wenzelm 2006-06-17 RuleCases.mutual_rule: ctxt; Term.internal; ProofContext.exports: simultaneous facts;
2006-06-17 dixon 2006-06-17 added interface for making term contexts.
2006-06-16 haftmann 2006-06-16 fixed symlink bug
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable; tuned;
2006-06-15 wenzelm 2006-06-15 Fixed type/term variables and polymorphic term abbreviations.
2006-06-15 wenzelm 2006-06-15 added variable.ML;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable;
2006-06-15 nipkow 2006-06-15 *** empty log message ***
2006-06-15 nipkow 2006-06-15 *** empty log message ***
2006-06-15 paulson 2006-06-15 the "all_theorems" option and some fixes
2006-06-15 paulson 2006-06-15 the enumerate operator
2006-06-14 webertj 2006-06-14 Jia Meng added to world map
2006-06-14 haftmann 2006-06-14 keyword update
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-14 haftmann 2006-06-14 slight adaptions for code generator
2006-06-14 haftmann 2006-06-14 slight adaptions
2006-06-14 haftmann 2006-06-14 slight refinements for code generator
2006-06-14 haftmann 2006-06-14 added hook for case const defs
2006-06-14 haftmann 2006-06-14 added codegen_simtype
2006-06-14 haftmann 2006-06-14 improvements in code generator
2006-06-13 wenzelm 2006-06-13 avoid global Drule.unvarify;
2006-06-13 wenzelm 2006-06-13 tuned interfaces; added invent_types; added import_types/terms;
2006-06-13 wenzelm 2006-06-13 added hyps_of; tuned;
2006-06-13 wenzelm 2006-06-13 added equiv;
2006-06-13 wenzelm 2006-06-13 (un)varify: tuned exceptions;
2006-06-13 wenzelm 2006-06-13 removed weak_eq_thm; added equiv_thm; removed obsolete unvarifyT; improved unvarify -- demands global context (cf. Logic.unvarify);
2006-06-13 wenzelm 2006-06-13 Drule.equiv_thm supercedes Drule.weak_eq_thm;
2006-06-13 wenzelm 2006-06-13 tuned;
2006-06-13 wenzelm 2006-06-13 avoid unqualified exception names; tuned;
2006-06-13 wenzelm 2006-06-13 ProjectRule now context dependent;
2006-06-13 wenzelm 2006-06-13 use Drule.unvarify instead of obsolete Drule.freeze_all;
2006-06-13 dixon 2006-06-13 corrected w.r.t. search order for subst.