isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

removed obsolete theory_of_sign, theory_of_thm;
2005-06-17, by wenzelm
PolyML.Compiler.printInAlphabeticalOrder := false;
2005-06-17, by wenzelm
Context.DATA_FAIL;
2005-06-17, by wenzelm
Context.PureN;
2005-06-17, by wenzelm
RuleCases.tactic;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
(RAW_)METHOD_CASES: RuleCases.tactic;
2005-06-17, by wenzelm
Theory.add_typedecls;
2005-06-17, by wenzelm
added map', fold;
2005-06-17, by wenzelm
Table.fold;
2005-06-17, by wenzelm
Symtab.fold;
2005-06-17, by wenzelm
type theory, theory_ref, exception THEORY and related operations imported from Context;
2005-06-17, by wenzelm
obsolete type sg is now an alias for Context.theory;
2005-06-17, by wenzelm
added theorem_space;
2005-06-17, by wenzelm
Context.theory_name;
2005-06-17, by wenzelm
added serial numbers;
2005-06-17, by wenzelm
removed obsolete pretty printers for Theory.theory, Sign.sg;
2005-06-17, by wenzelm
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
2005-06-17, by wenzelm
added type theory: generic theory contexts with unique identity,
2005-06-17, by wenzelm
removed Pure/theory_data.ML;
2005-06-17, by wenzelm
added Id;
2005-06-17, by wenzelm
Theory.merge;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
Context.theory_name;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
replaced obsolete theory_of_sign by theory_of_thm;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
refer to HOL4_PROOFS setting;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
accomodate identification of type Sign.sg and theory;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
renamed sg_ref to thy_ref;
2005-06-17, by wenzelm
obsolete;
2005-06-17, by wenzelm
obsolete (see context.ML);
2005-06-17, by wenzelm
(removed experimental file)
2005-06-17, by haftmann
updated;
2005-06-17, by wenzelm
Multiple subgoals working.
2005-06-17, by quigley
migrated theory headers to new format
2005-06-17, by haftmann
grammar fix
2005-06-17, by paulson
removed redundant "open" declarations
2005-06-17, by paulson
tuned;
2005-06-16, by wenzelm
a few new integer lemmas
2005-06-16, by paulson
*** empty log message ***
2005-06-16, by nipkow
isa-migrate ++
2005-06-16, by haftmann
*** empty log message ***
2005-06-16, by nipkow
*** empty log message ***
2005-06-16, by nipkow
isa-migrate ++
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
added macos emacs hints
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
Domain package uses ContProc for beta reduction
2005-06-15, by huffman
allow theorem attributes on fixpat declarations
2005-06-15, by huffman
fixrec package now handles mutually-recursive definitions
2005-06-15, by huffman
(undone experimental changes)
2005-06-15, by haftmann
subclassing done
2005-06-15, by haftmann
int -> IntInf.int
2005-06-15, by chaieb
added lemmas
2005-06-15, by nipkow
*** empty log message ***
2005-06-15, by nipkow
documented DUMMY
2005-06-15, by nipkow

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle