isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Command.memo including physical interrupts (unlike Lazy.lazy);
2012-04-05, by wenzelm
tuned;
2012-04-05, by wenzelm
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04, by wenzelm
proper signature constraint;
2012-04-04, by wenzelm
tuned comments;
2012-04-04, by wenzelm
separate module for prover command execution;
2012-04-04, by wenzelm
tuned;
2012-04-04, by wenzelm
fix typo in ML structure name
2012-04-04, by huffman
removed obsolete isar-overview manual;
2012-04-04, by wenzelm
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
2012-04-04, by sultana
merged
2012-04-04, by bulwahn
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-04-04, by bulwahn
improved equality check for modes in predicate compiler
2012-04-04, by bulwahn
rename ML structure to avoid shadowing earlier name
2012-04-04, by huffman
add type annotations to make SML happy (cf. ec6187036495)
2012-04-04, by huffman
merged
2012-04-03, by huffman
new transfer proof method
2012-04-03, by huffman
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-03, by huffman
prefer prog-prove, suppress isar-overview;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
formal integration of "prog-prove" manual;
2012-04-03, by wenzelm
prefer static dependencies;
2012-04-03, by wenzelm
merged
2012-04-03, by huffman
modernized obsolete old-style theory name with proper new-style underscore
2012-04-03, by huffman
removed use of CharVector in generated parser, to make SMLNJ happy
2012-04-03, by sultana
avoid duplicate PIDE markup;
2012-04-03, by wenzelm
less intrusive visibility;
2012-04-03, by wenzelm
more robust re-import wrt. non-HHF assumptions;
2012-04-03, by wenzelm
consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
2012-04-03, by wenzelm
close context elements via Expression.cert/read_declaration;
2012-04-03, by wenzelm
merged
2012-04-03, by wenzelm
added me to isatest email list
2012-04-03, by sultana
new package Lifting - initial commit
2012-04-03, by kuncar
add floor/ceiling lemmas suggested by René Thiemann
2012-04-03, by huffman
made sure that " is shown in tutorial text
2012-04-03, by nipkow
merged
2012-04-02, by Christian Urban
tuned proofs
2012-04-02, by Christian Urban
merged
2012-04-02, by nipkow
towards showing " in the tutorial
2012-04-02, by nipkow
tuned proof in order to avoid warning message
2012-04-02, by Christian Urban
remove unnecessary qualifiers on names
2012-04-02, by huffman
add lemma Suc_1
2012-04-02, by huffman
merged
2012-04-02, by berghofe
Require "For" keyword to be followed by at least one whitespace, to avoid that
2012-04-02, by berghofe
normalize defs (again, cf. 008b7858f3c0);
2012-04-03, by wenzelm
some context examples;
2012-04-03, by wenzelm
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
2012-04-03, by wenzelm
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
2012-04-03, by wenzelm
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
2012-04-03, by wenzelm
better drop background syntax if entity depends on parameters;
2012-04-03, by wenzelm
more uniform abbrev vs. define;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
clarified generic_const vs. close_schematic_term;
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more uniform theory_abbrev with const_declaration;
2012-04-03, by wenzelm
avoid const_declaration in aux. context (cf. locale_foundation);
2012-04-03, by wenzelm
clarified background_foundation vs. theory_foundation (with const_declaration);
2012-04-03, by wenzelm
tuned;
2012-04-03, by wenzelm
more general standard_declaration;
2012-04-02, by wenzelm

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

isabelle