isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

normal_form to lemma test
2006-06-30, by nipkow
normalization uses refl now
2006-06-30, by nipkow
Removed some incorrect axioms.
2006-06-30, by mengj
fixed stale theory bug
2006-06-30, by haftmann
slight refinements
2006-06-30, by haftmann
refinement in instance command
2006-06-30, by haftmann
small change in class_package
2006-06-30, by haftmann
added the "th" field to datatype Clause
2006-06-29, by paulson
fixed the "factor" method
2006-06-29, by paulson
new function norm_term
2006-06-29, by nipkow
new method "normalization"
2006-06-29, by nipkow
use -f in cp to overwrite read-only files (e.g. .svn in document/)
2006-06-29, by kleing
world map now transparent
2006-06-28, by webertj
improvements in Classpackage
2006-06-28, by haftmann
reduced code, better instance command
2006-06-28, by haftmann
slight improvements in code generation
2006-06-28, by haftmann
added lookup function for parameters
2006-06-28, by haftmann
disjunctive wellfoundedness
2006-06-28, by paulson
class package refinements, slight code generation refinements
2006-06-27, by haftmann
added class projection
2006-06-27, by haftmann
slight improvement
2006-06-27, by haftmann
replaced subgraph by project
2006-06-27, by haftmann
fix/fixes: tuned type constraints;
2006-06-24, by wenzelm
minor tuning of definitions/proofs;
2006-06-24, by wenzelm
fixed translations for _MapUpd: CONST;
2006-06-24, by wenzelm
beautification
2006-06-23, by nipkow
added webmaster
2006-06-23, by haftmann
Introduction of Ramsey's theorem
2006-06-23, by paulson
Removed debugging code.
2006-06-22, by ballarin
Improved handling of defines imported in duplicate.
2006-06-22, by ballarin
new standard dir structure
2006-06-22, by kleing
world map updated
2006-06-21, by webertj
world map updated
2006-06-21, by webertj
Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
2006-06-21, by krauss
fixed bug resolving Haskell names
2006-06-21, by haftmann
fixed error bug
2006-06-21, by haftmann
renamed thy data
2006-06-21, by haftmann
Added split_cong rule
2006-06-21, by krauss
hyps better than prems
2006-06-21, by haftmann
fixed sml/nj value restriction problem
2006-06-20, by haftmann
Restructured locales with predicates: import is now an interpretation.
2006-06-20, by ballarin
Fixed another variable order bug...
2006-06-20, by krauss
switched to open locales for classes
2006-06-20, by haftmann
switched to open locales for classes
2006-06-20, by haftmann
refrain from reforming TFL -- back to previous revision;
2006-06-19, by wenzelm
added declare_thm, thm_context;
2006-06-19, by wenzelm
eliminated freeze/varify in favour of Variable.import/export/trade;
2006-06-19, by wenzelm
world map updated
2006-06-19, by webertj
world map updated
2006-06-19, by webertj
Fixed name clash.
2006-06-19, by krauss
world map updated
2006-06-19, by webertj
matchers: try pattern_matchers only *after* general matching (The
2006-06-19, by wenzelm
ProofContext.exports: simultaneous facts;
2006-06-17, by wenzelm
moved internal/skolem to term.ML;
2006-06-17, by wenzelm
mutual_rule: proper context;
2006-06-17, by wenzelm
export: simultaneous facts, refer to Variable.export;
2006-06-17, by wenzelm
ProofContext.exports: simultaneous facts;
2006-06-17, by wenzelm
Variable.importT_inst;
2006-06-17, by wenzelm
standard: simultaneous facts;
2006-06-17, by wenzelm
added singleton;
2006-06-17, by wenzelm
major reworking of export functionality -- based on Term/Thm.generalize;
2006-06-17, by wenzelm
added generalize rule;
2006-06-17, by wenzelm
added exists_subtype;
2006-06-17, by wenzelm
added generalize rule;
2006-06-17, by wenzelm
Term.skolem;
2006-06-17, by wenzelm
Term.internal;
2006-06-17, by wenzelm
ProofContext.export: singleton;
2006-06-17, by wenzelm
RuleCases.mutual_rule: ctxt;
2006-06-17, by wenzelm
RuleCases.mutual_rule: ctxt;
2006-06-17, by wenzelm
added interface for making term contexts.
2006-06-17, by dixon
fixed symlink bug
2006-06-16, by haftmann
ProofContext: moved variable operations to struct Variable;
2006-06-15, by wenzelm
Fixed type/term variables and polymorphic term abbreviations.
2006-06-15, by wenzelm
added variable.ML;
2006-06-15, by wenzelm
ProofContext: moved variable operations to struct Variable;
2006-06-15, by wenzelm
*** empty log message ***
2006-06-15, by nipkow
*** empty log message ***
2006-06-15, by nipkow
the "all_theorems" option and some fixes
2006-06-15, by paulson
the enumerate operator
2006-06-15, by paulson
Jia Meng added to world map
2006-06-14, by webertj
keyword update
2006-06-14, by haftmann
slight adaption for code generator
2006-06-14, by haftmann
slight adaptions for code generator
2006-06-14, by haftmann
slight adaptions
2006-06-14, by haftmann
slight refinements for code generator
2006-06-14, by haftmann
added hook for case const defs
2006-06-14, by haftmann
added codegen_simtype
2006-06-14, by haftmann
improvements in code generator
2006-06-14, by haftmann
avoid global Drule.unvarify;
2006-06-13, by wenzelm
tuned interfaces;
2006-06-13, by wenzelm
added hyps_of;
2006-06-13, by wenzelm
added equiv;
2006-06-13, by wenzelm
(un)varify: tuned exceptions;
2006-06-13, by wenzelm
removed weak_eq_thm;
2006-06-13, by wenzelm
Drule.equiv_thm supercedes Drule.weak_eq_thm;
2006-06-13, by wenzelm
tuned;
2006-06-13, by wenzelm
avoid unqualified exception names;
2006-06-13, by wenzelm
ProjectRule now context dependent;
2006-06-13, by wenzelm
use Drule.unvarify instead of obsolete Drule.freeze_all;
2006-06-13, by wenzelm
corrected w.r.t. search order for subst.
2006-06-13, by dixon
Corrected search order for zippers.
2006-06-13, by dixon
new results
2006-06-13, by paulson
removal of the obsolete "infinite_nonempty"
2006-06-13, by paulson
tuned;
2006-06-12, by wenzelm
added declare_typ;
2006-06-12, by wenzelm
tuned;
2006-06-12, by wenzelm
tuned interfaces;
2006-06-12, by wenzelm
added matchers, matches_list;
2006-06-12, by wenzelm
removed matches_seq -- didn't quite work;
2006-06-12, by wenzelm
Unify.matches_list;
2006-06-12, by wenzelm
tuned Seq/Envir/Unify interfaces;
2006-06-12, by wenzelm
fixed subst step;
2006-06-12, by wenzelm
avoid accidental binding of ?Jmp;
2006-06-12, by wenzelm
added lemma fresh_unit to Nominal.thy
2006-06-12, by urbanc
Added fresh_guess_tac.
2006-06-12, by berghofe
Removed comments around declaration of fresh_guess method.
2006-06-12, by berghofe
Added "evaluation" method.
2006-06-12, by berghofe
updated keywords
2006-06-12, by haftmann
made smlnj happy;
2006-06-12, by wenzelm
fixed smlnj incompat.
2006-06-12, by haftmann