isabelle: Graph

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

changed import order
2006-11-07, by haftmann
Added a (stub of a) function tutorial
2006-11-07, by krauss
Preparations for making "lexicographic_order" part of "fun"
2006-11-07, by krauss
renamed 'const_syntax' to 'notation';
2006-11-07, by wenzelm
'const_syntax' command: allow fixed variables, renamed to 'notation';
2006-11-07, by wenzelm
replaced const_syntax by notation, which operates on terms;
2006-11-07, by wenzelm
Isar.context: proper error;
2006-11-07, by wenzelm
replaced const_syntax by notation, which operates on terms;
2006-11-07, by wenzelm
read_const: include type;
2006-11-07, by wenzelm
renamed 'const_syntax' to 'notation';
2006-11-07, by wenzelm
updated;
2006-11-07, by wenzelm
Adapted to changes in FixedPoint theory.
2006-11-07, by berghofe
method exported
2006-11-07, by krauss
updated NEWS
2006-11-07, by krauss
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
2006-11-07, by krauss
added gfx
2006-11-07, by haftmann
dropped blastdata.ML
2006-11-06, by haftmann
(adjustions)
2006-11-06, by haftmann
two further lemmas on split
2006-11-06, by haftmann
removed dependency of ord on eq
2006-11-06, by haftmann
removed itrev as inlining theorem
2006-11-06, by haftmann
added state monad to HOL library
2006-11-06, by haftmann
code generator module naming improved
2006-11-06, by haftmann
(continued)
2006-11-06, by haftmann
(continued)
2006-11-06, by haftmann
minor cleanup
2006-11-06, by krauss
case_tr: do not intern already internal consts;
2006-11-05, by wenzelm
updated;
2006-11-05, by wenzelm
removed isactrlconst;
2006-11-05, by wenzelm
instantiate: avoid global references;
2006-11-05, by wenzelm
added const_syntax_name;
2006-11-05, by wenzelm
removed obsolete first_duplicate;
2006-11-05, by wenzelm
added syntax_name;
2006-11-05, by wenzelm
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
refined algorithm
2006-10-31, by haftmann
simplified preprocessor framework
2006-10-31, by haftmann
cleanup
2006-10-31, by haftmann
*** empty log message ***
2006-10-31, by haftmann
fixed type signature of Type.varify
2006-10-31, by haftmann
dropped junk
2006-10-31, by haftmann
disabled some code generation (an intermeidate solution)
2006-10-31, by haftmann
adapted to new serializer syntax
2006-10-31, by haftmann
added Equals_conv
2006-10-31, by haftmann
cleaned up
2006-10-31, by haftmann
adaptions to changes in preprocessor
2006-10-31, by haftmann
dropped nth_update
2006-10-31, by haftmann
Purely cosmetic
2006-10-30, by paulson
new file for defining functions in the lambda-calculus
2006-10-30, by urbanc
Added "recdef_wf" and "simp" attribute to "wf_measures"
2006-10-26, by krauss
Removed debugging output
2006-10-26, by krauss
removed free "x" from termination goal...
2006-10-26, by krauss
Added "measures" combinator for lexicographic combinations of multiple measures.
2006-10-26, by krauss
Conversion to clause form now tolerates Boolean variables without looping.
2006-10-26, by paulson