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 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Moved definition of normal forms to new NormalForm theory.
2007-09-06, by berghofe
Added Standardization theory.
2007-09-06, by berghofe
New code generator setup (taken from Library/Executable_Real.thy,
2007-09-06, by berghofe
Added code generator setup (taken from Library/Executable_Rat.thy,
2007-09-06, by berghofe
Integrated code generator setup into RealDef theory.
2007-09-06, by berghofe
Integrated code generator setup into Rational theory.
2007-09-06, by berghofe
Integrated Executable_Rat and Executable_Real theories into
2007-09-06, by berghofe
use preferences.ML: do setmp *here*, to capture intended default values;
2007-09-05, by wenzelm
tuned;
2007-09-05, by wenzelm
modified proofs so that they are not using claset()
2007-09-05, by urbanc
tuned lemma; replaced !! by arbitrary
2007-09-04, by nipkow
Improved comment.
2007-09-04, by ballarin
Documented function package in IsarRef-manual.
2007-09-03, by krauss
added variations on infinite descent
2007-09-03, by nipkow
fixed Rat.inv
2007-09-03, by haftmann
fixed Rat.inv
2007-09-03, by haftmann
fix sgn_div_norm class
2007-09-02, by huffman
made theorem-references safe
2007-09-02, by urbanc
removed unused join_mode;
2007-09-01, by wenzelm
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
2007-09-01, by wenzelm
removed obsolete ML bindings;
2007-09-01, by wenzelm
linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;
2007-09-01, by wenzelm
mono_Int/Un: proper proof, avoid illegal schematic type vars;
2007-09-01, by wenzelm
removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;
2007-09-01, by wenzelm
added singleton check_typ/term/prop;
2007-09-01, by wenzelm
removed obsolete read/cert variations (cf. Syntax.read/check);
2007-09-01, by wenzelm
replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
2007-09-01, by wenzelm
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-09-01, by wenzelm
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-09-01, by wenzelm
*** empty log message ***
2007-09-01, by nipkow

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

isabelle