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

fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
2006-11-05, by wenzelm
Sign.const_syntax_name;
2006-11-05, by wenzelm
added gfx
2006-11-05, by haftmann
removed checkpoint interface;
2006-11-04, by wenzelm
String.compare: slow version -- performance test;
2006-11-04, by wenzelm
replaced apply_copy by apply';
2006-11-04, by wenzelm
removed is_Trueprop (use can dest_Trueprop'' instead);
2006-11-04, by wenzelm
removed is_Trueprop (use can dest_Trueprop'' instead);
2006-11-04, by wenzelm
updated;
2006-11-04, by wenzelm
HOL_USEDIR_OPTIONS: -p 1 by default;
2006-11-04, by wenzelm
tuned;
2006-11-04, by wenzelm
* October 2006: Stefan Hohe, TUM;
2006-11-04, by wenzelm
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
2006-11-04, by wenzelm
optional argument for timespan (default 100);
2006-11-04, by wenzelm
added at-mac-poly-e, at64-poly-e;
2006-11-04, by wenzelm
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
2006-11-04, by huffman
new Deriv.thy contains stuff from Lim.thy
2006-11-04, by huffman
re-added simpdata.ML
2006-11-03, by haftmann
new ML serializer
2006-11-03, by haftmann
fixed problem with eta-expansion
2006-11-03, by haftmann
tuned
2006-11-03, by haftmann
fixed problem with variable names
2006-11-03, by haftmann
tightened notion of function equations
2006-11-03, by haftmann
dropped name_mangler.ML
2006-11-03, by haftmann
some example tweaking
2006-11-03, by haftmann
added particular test for partially applied case constants
2006-11-03, by haftmann
improved evaluation setup
2006-11-03, by haftmann
adapted to changes in codegen_data.ML
2006-11-03, by haftmann
added code gen II
2006-11-03, by haftmann
simplified reasoning tools setup
2006-11-03, by haftmann
dropped prop_cs
2006-11-03, by haftmann
dropped equals_conv for nbe
2006-11-03, by haftmann
first version of style guide
2006-11-03, by haftmann
continued tutorial
2006-11-03, by haftmann
added serialization keywords
2006-11-03, by haftmann
bugfix to zipto: left and right were wrong way around.
2006-11-02, by dixon
added sum_squared
2006-11-02, by nipkow
changed a misplaced "also" to a "moreover" (caused a loop somehow)
2006-11-01, by urbanc
changed to not compile Iteration and Recursion, but Lam_Funs instead
2006-11-01, by urbanc
move DERIV_sumr from Series.thy to Lim.thy
2006-11-01, by huffman
generalize type of lemma isCont_Id
2006-11-01, by huffman
new proof of Bseq_NSbseq using transfer
2006-11-01, by huffman
changed to use Lam_Funs
2006-11-01, by urbanc
clauses for iff-introduction, unfortunately useless
2006-11-01, by paulson
tuned
2006-11-01, by urbanc
Numerous cosmetic changes.
2006-11-01, by paulson
not needed anymore
2006-11-01, by urbanc
these files are superseded by the internal recursion combinator and the file Lam_Funs.thy
2006-11-01, by urbanc
More blacklisting
2006-11-01, by paulson
added lexicographic_order tactic
2006-11-01, by bulwahn
new SML serializer
2006-10-31, by haftmann
clarified make_term interface
2006-10-31, by haftmann
introduced CodegenData.add_func_legacy
2006-10-31, by haftmann
cleaned up
2006-10-31, by haftmann
adapted seralizer syntax
2006-10-31, by haftmann
adapted to new serializer syntax
2006-10-31, by haftmann
constructing proof
2006-10-31, by haftmann
dropped constructiv `->
2006-10-31, by haftmann
new serialization syntax; experimental extensions
2006-10-31, by haftmann
refined
2006-10-31, by haftmann

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

isabelle