Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned comments;
2014-10-16, by wenzelm
support line context with depth;
2014-10-16, by wenzelm
proper type comparison (amending cd4439d8799c);
2014-10-16, by wenzelm
tuned;
2014-10-16, by wenzelm
tuned
2014-10-16, by haftmann
standard elimination rule for even
2014-10-16, by haftmann
tuned facts on even and power
2014-10-16, by haftmann
restructured
2014-10-16, by haftmann
even more cleanup
2014-10-16, by haftmann
made SML/NJ happier
2014-10-16, by blanchet
made SML/NJ happier
2014-10-15, by blanchet
tuned whitespace
2014-10-15, by blanchet
buffer_line_context via untyped access;
2014-10-14, by wenzelm
access class hierarchy;
2014-10-14, by wenzelm
legacy cleanup
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
purely algebraic characterization of even and odd
2014-10-14, by haftmann
document 'sel_transfer'
2014-10-14, by desharna
generate 'sel_transfer' for (co)datatypes
2014-10-14, by desharna
add 'kind' to 'cr_sugar'
2014-10-14, by desharna
add 'fp_bnf' to 'bnf_sugar'
2014-10-14, by desharna
preserve the structure of 'set_intros' theorem in ML
2014-10-14, by desharna
preserve the structure of 'map_sel' theorem in ML
2014-10-14, by desharna
preserve the structure of 'set_sel' theorem in ML
2014-10-14, by desharna
Fixed bug in waldmeister skolemization
2014-10-14, by steckerm
tuned signature;
2014-10-14, by wenzelm
tuned signature;
2014-10-13, by wenzelm
merged
2014-10-13, by wenzelm
tuned signature;
2014-10-13, by wenzelm
tuned signature;
2014-10-13, by wenzelm
obsolete;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
clarified load order;
2014-10-13, by wenzelm
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-10-13, by wenzelm
support for indirections (defined entries), e.g. relevant for quickcheck and its sub-plugins;
2014-10-13, by wenzelm
support for named plugins for definitional packages;
2014-10-13, by wenzelm
relaxed class constraints for exp
2014-10-13, by immler
tuned
2014-10-13, by nipkow
special treatment of extensionality in minimizer
2014-10-12, by blanchet
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
2014-10-12, by blanchet
made SML/NJ happier
2014-10-12, by blanchet
leftover from 3ccafeb9a1d1
2014-10-12, by haftmann
some more facts on divisibility
2014-10-12, by haftmann
generalized and consolidated some theorems concerning divisibility
2014-10-12, by haftmann
eliminiated clone
2014-10-12, by haftmann
more facts about abstract divisibility
2014-10-12, by haftmann
specialized specification: avoid trivial instances
2014-10-10, by haftmann
more foundational definition for predicate even
2014-10-09, by haftmann
New example Bubblesort
2014-10-10, by nipkow
formally completeted set of experimental static evaluation functions
2014-10-09, by haftmann
merged
2014-10-09, by wenzelm
afford slightly bigger JVM stack (see also f7ba30a816b9);
2014-10-09, by wenzelm
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
2014-10-09, by wenzelm
prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
2014-10-09, by wenzelm
proper @{cite} with bibtex entry (unchecked comment);
2014-10-09, by wenzelm
fix document generation in Code_Test
2014-10-09, by hoelzl
merged
2014-10-08, by wenzelm
eliminated some exotic combinators;
2014-10-08, by wenzelm
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-08, by wenzelm
tuned;
2014-10-08, by wenzelm
tuned;
2014-10-08, by wenzelm
clarified messages depending on options;
2014-10-08, by wenzelm
simplified "sos" method;
2014-10-08, by wenzelm
tuned signature;
2014-10-08, by wenzelm
tuned spelling;
2014-10-08, by wenzelm
add Linear Temporal Logic on Streams
2014-10-08, by hoelzl
move Code_Test to HOL/Library;
2014-10-08, by Andreas Lochbihler
proper bibliography;
2014-10-08, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
more bibtex entries;
2014-10-07, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
tuned whitespace;
2014-10-07, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
clarified whitespace;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
merged
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more symbols;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
added update_cartouches tool;
2014-10-07, by wenzelm
removed pointless regexp flags;
2014-10-07, by wenzelm
fix document generation for HOL-Probability
2014-10-07, by hoelzl
move Stream theory from Datatype_Examples to Library
2014-10-07, by hoelzl
add Giry monad
2014-10-07, by hoelzl
tuned
2014-10-06, by nipkow
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
2014-10-06, by wenzelm
merged
2014-10-06, by nipkow
tuned spaces
2014-10-06, by nipkow
avoid creating needless skolemization steps for SPASS
2014-10-06, by blanchet
get rid of 'individual' type in DFG proofs
2014-10-06, by blanchet
slightly nicer names
2014-10-06, by blanchet
strengthened 'moura' method
2014-10-06, by blanchet
improved unskolemization of SPASS problems
2014-10-06, by blanchet
more total parser;
2014-10-06, by wenzelm
more defensive error handling -- token marker must not crash;
2014-10-06, by wenzelm
merged
2014-10-06, by wenzelm
documentation of @{cite} and cite_macro;
2014-10-06, by wenzelm
completion for bibtex entries;
2014-10-06, by wenzelm
more accurate item name, depending on kind;
2014-10-06, by wenzelm
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
2014-10-06, by wenzelm
tuned signature;
2014-10-06, by wenzelm
add measure space for (coinductive) streams
2014-10-06, by hoelzl
add type for probability mass functions, i.e. discrete probability distribution
2014-10-06, by hoelzl
refactor 'map_sel_thms' and 'set_sel_thms'
2014-10-06, by desharna
rename 'xtor_rel_thms' to 'xtor_rels'
2014-10-06, by desharna
rename 'xtor_set_thmss' to 'xtor_setss'
2014-10-06, by desharna
rename 'xtor_map_thms' to 'xtor_maps'
2014-10-06, by desharna
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
2014-10-06, by desharna
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
2014-10-06, by desharna
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
2014-10-06, by desharna
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
2014-10-06, by desharna
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
2014-10-06, by desharna
add 'set_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'common_set_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_co_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'common_rel_co_induct' to 'fp_sugar'
2014-10-06, by desharna
add 'co_rec_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'co_rec_disc_iffs' to 'fp_sugar'
2014-10-06, by desharna
add 'disc_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'case_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'ctr_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'set_cases' to 'fp_sugar'
2014-10-06, by desharna
add 'set_intros' to 'fp_sugar'
2014-10-06, by desharna
add 'set_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'set_thms' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_cases' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_intros' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'map_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'map_disc_iffs' to 'fp_sugar'
2014-10-06, by desharna
code preprocessor tracing also for function transformers
2014-10-05, by haftmann
basic support for fully static evaluator generation without dynamic compiler invocation
2014-10-05, by haftmann
split dynamic from static context
2014-10-05, by haftmann
more refs;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
NEWS;
2014-10-05, by wenzelm
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
citation tooltip/hyperlink based on open buffers with .bib files;
2014-10-05, by wenzelm
bibtex support in ML: document antiquotation @{cite} with markup;
2014-10-05, by wenzelm
maintain Document_Model.bibtex_entries;
2014-10-05, by wenzelm
more advanced NEWS tree structure and folding;
2014-10-05, by wenzelm
merged;
2014-10-04, by wenzelm
NEWS;
2014-10-04, by wenzelm
tuned output;
2014-10-04, by wenzelm
proper treatment of @comment (amending 402a8e8107a7);
2014-10-04, by wenzelm
mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);
2014-10-04, by wenzelm
more total chunk_line: recovery via ignored_line;
2014-10-04, by wenzelm
more explicit comments;
2014-10-04, by wenzelm
clarified nesting of delimiters;
2014-10-04, by wenzelm
fields are case-insensitive;
2014-10-04, by wenzelm
clarified nesting of delimiters;
2014-10-04, by wenzelm
more explicit chunk name;
2014-10-04, by wenzelm
clarified Chunk -- avoid ooddities;
2014-10-04, by wenzelm
support for bibtex token markup;
2014-10-04, by wenzelm
more explicit item kind;
2014-10-03, by wenzelm
strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;
2014-10-03, by wenzelm
SideKick parser for bibtex entries;
2014-10-03, by wenzelm
more buffer.isEditable checks;
2014-10-03, by wenzelm
context menu for bibtex entries;
2014-10-03, by wenzelm
some support for bibtex files;
2014-10-02, by wenzelm
tuned
2014-10-03, by nipkow
tuned
2014-10-03, by nipkow
accomplish potentially case-insenstive file systems for Scala
2014-10-02, by haftmann
tuned
2014-10-02, by nipkow
merge
2014-10-02, by blanchet
more precise lemma insertion
2014-10-02, by blanchet
insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
2014-10-02, by blanchet
avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition
2014-10-02, by blanchet
eliminate duplicate hypotheses (which can arise due to (un)clausification)
2014-10-02, by blanchet
formal lcm definition for polynomials
2014-10-02, by haftmann
moved lemmas out of Int.thy which have nothing to do with int
2014-10-02, by haftmann
redundant: dropped
2014-10-02, by haftmann
tuned Heap_Monad.successE
2014-10-02, by haftmann
documentation
2014-10-02, by blanchet
fixed a few mistakes in the documentation
2014-10-02, by blanchet
tuning
2014-10-02, by blanchet
'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3
2014-10-02, by blanchet
actually finish after closing, e.g. relevant for consecutive (**)(**);
2014-10-01, by wenzelm
tuned
2014-09-30, by nipkow
tuned;
2014-09-30, by wenzelm
tuned
2014-09-30, by nipkow
don't call 'hd' on a possibly empty list
2014-09-30, by blanchet
proper types for applied variables, for typed formats (TFF0, DFG)
2014-09-30, by blanchet
don't affect other subgoals with 'auto' in one-liner proofs
2014-09-30, by blanchet
tuned output in case of one-liner failure
2014-09-30, by blanchet
updated docs with two provers: veriT and Zipperposition
2014-09-30, by blanchet
give more facts to veriT -- it seems to be able to cope with them
2014-09-30, by blanchet
use native encoding with Vampire -- modern versions handle types better than the old ones
2014-09-30, by blanchet
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
2014-09-30, by blanchet
correct inlining in veriT's subproofs.
2014-09-30, by fleury
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
2014-09-30, by blanchet
tuning
2014-09-30, by blanchet
tuning
2014-09-30, by blanchet
keep rules with no premises in Isar proofs from veriT
2014-09-30, by blanchet
correct indexing in the presence of lambda-lifting
2014-09-30, by blanchet
merged
2014-09-29, by nipkow
tuned
2014-09-29, by nipkow
merge
2014-09-29, by blanchet
support hypotheses with schematics in Isar proofs
2014-09-29, by blanchet
tuned
2014-09-29, by nipkow
simplified and repaired veriT index handling code
2014-09-29, by blanchet
made 'moura' tactic more powerful
2014-09-29, by blanchet
fixed wrong optimization (wrong because it may affect the sequent's conclusion)
2014-09-29, by blanchet
merge
2014-09-29, by blanchet
added option to get cleaner SPASS proofs
2014-09-29, by blanchet
parse back type of SPASS proof variables
2014-09-29, by blanchet
make sure no '__' suffixes make it until Isar proof
2014-09-29, by blanchet
rename skolem symbols in the negative case as well
2014-09-29, by blanchet
reintroduced 'rel_cases' in docs
2014-09-29, by blanchet
added options to Mirabelle
2014-09-29, by blanchet
tuning
2014-09-29, by blanchet
faster machine for slow/bulky polyml-5.3.0 tests (notably HOL-Proofs);
2014-09-29, by wenzelm
pro-forma support for polyml-5.5.3 (presently SVN 1960);
2014-09-29, by wenzelm
corrected white-space accident
2014-09-29, by haftmann
tuned
2014-09-28, by haftmann
moved to HOL and generalized
2014-09-28, by haftmann
merged
2014-09-26, by wenzelm
proper range for Antiq tokens;
2014-09-26, by wenzelm
support for sub-expression markup;
2014-09-26, by wenzelm
tuned message;
2014-09-26, by wenzelm
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar with empty substructures
2014-09-26, by desharna
add attribute 'case_names' to 'set_case'
2014-09-26, by desharna
make 'case_transfer' tactic more robust
2014-09-26, by desharna
more correct precedence of do-notation
2014-09-25, by haftmann
merged
2014-09-25, by wenzelm
save image as PNG or PDF;
2014-09-25, by wenzelm
support for PNG output;
2014-09-25, by wenzelm
more isatests (on lxbroy4);
2014-09-25, by wenzelm
document 'corec_transfer'
2014-09-25, by desharna
generate 'corec_transfer' for codatatypes
2014-09-25, by desharna
document 'rec_transfer'
2014-09-25, by desharna
generate 'rec_transfer' for datatypes
2014-09-25, by desharna
generate 'dtor_corec_transfer' for codatatypes
2014-09-25, by desharna
generate 'ctor_rec_transfer' for datatypes
2014-09-25, by desharna
goal generation for xtor_co_rec_transfer
2014-09-01, by traytel
commented out some tests that require external tools (e.g. ghc)
2014-09-25, by blanchet
added useful options to CVC4
2014-09-25, by blanchet
subscribe for isatest
2014-09-25, by traytel
even more deads go to the end (continuation of e3a01b73579f)
2014-09-25, by traytel
added function size1
2014-09-25, by nipkow
added lemmas
2014-09-24, by haftmann
tuned
2014-09-24, by haftmann
avoid type variable name clash
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
2014-09-24, by blanchet
improved 'bnf' parser
2014-09-24, by blanchet
updated SMT certificates
2014-09-24, by blanchet
allow homogeneous nesting for SMT (co)datatypes
2014-09-24, by blanchet
interleave (co)datatypes in the right order w.r.t. dependencies
2014-09-24, by blanchet
rule out nested (co)recursion for SMT (co)datatypes
2014-09-24, by blanchet
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
simpler proof
2014-09-24, by blanchet
added nice standard syntax
2014-09-24, by nipkow
clarified timeout for isatest;
2014-09-22, by wenzelm
merged
2014-09-22, by wenzelm
discontinued old "xnum" token category;
2014-09-22, by wenzelm
added csdp-6.x for proof method (sos csdp);
2014-09-22, by wenzelm
examples for local CSDP executable;
2014-09-22, by wenzelm
clarified SOS tool setup vs. examples;
2014-09-22, by wenzelm
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
2014-09-22, by desharna
merged
2014-09-22, by wenzelm
clarified ISABELLE_POLYML;
2014-09-22, by wenzelm
drop workaround addressed by d0d3c30806b4
2014-09-22, by Andreas Lochbihler
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-21, by wenzelm
more standard Isabelle/ML operations;
2014-09-21, by wenzelm
tuned;
2014-09-21, by wenzelm
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-21, by haftmann
corrected slip in documentation
2014-09-21, by haftmann
Removed double space
2014-09-20, by steckerm
Changed proof method to auto for custom Waldmeister lemma
2014-09-20, by steckerm
Minor fixes in ATP_Waldmeister
2014-09-20, by steckerm
Made encoded type for apply less restrictive
2014-09-20, by steckerm
Updated fix_name function
2014-09-20, by steckerm
Added support for partial function application
2014-09-20, by steckerm
Improved equality handling in skolemization
2014-09-20, by steckerm
Re-added hypothesis argument to problem generation
2014-09-20, by steckerm
always annotate potentially polymorphic Haskell numerals
2014-09-18, by haftmann
tuned
2014-09-18, by haftmann
simplified and tuned using signed_string_of_int
2014-09-18, by haftmann
tuned data structure
2014-09-18, by haftmann
tuning
2014-09-19, by blanchet
documented limitations
2014-09-19, by blanchet
more honest 'primcorec' -- don't parse a theorem name that is then ignored
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
added a few tests for 'old_datatype'
2014-09-19, by blanchet
reintroduced old setup for size of basic types
2014-09-19, by blanchet
keep obsolete interpretations in Main, to avoid merge trouble
2014-09-19, by blanchet
made new 'primrec' bootstrapping-capable
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
typo
2014-09-19, by traytel
regression tests for n2m
2014-09-19, by traytel
merged
2014-09-19, by Andreas Lochbihler
add lemma
2014-09-18, by Andreas Lochbihler
tuned imports
2014-09-18, by blanchet
removed debugging junk
2014-09-18, by blanchet
help AFP entry 'Free-Groups' to compile
2014-09-18, by blanchet
reintroduced an instantiation of 'size' for 'numerals'
2014-09-18, by blanchet
use selector
2014-09-18, by blanchet
moved old 'size' generator together with 'old_datatype'
2014-09-18, by blanchet
moved datatype realizer to 'old_datatype' and colleagues
2014-09-18, by blanchet
careful with op = in n2m (actually by Dmitriy Traytel)
2014-09-18, by blanchet
fixed attribute name in docs (thanks to Andreas Lochbihler)
2014-09-18, by blanchet
updated NEWS
2014-09-18, by blanchet
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
2014-09-18, by blanchet
increased 'HOL-Proofs' timeout
2014-09-18, by blanchet
made 'mk_pointfree' work again in local theories
2014-09-18, by blanchet
fixed authorship
2014-09-18, by blanchet
product over monoids for lists
2014-09-18, by haftmann
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-09-18, by blanchet
more meaningful record tests
2014-09-18, by blanchet
updated SMT certificates
2014-09-18, by blanchet
tuning
2014-09-17, by blanchet
take out selectors for records -- for derived records, these don't quite have the right type
2014-09-17, by blanchet
register Isabelle selectors as SMT selectors when possible
2014-09-17, by blanchet
added codatatype support for CVC4
2014-09-17, by blanchet
added interface for CVC4 extensions
2014-09-17, by blanchet
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
2014-09-17, by blanchet
tweaked compatibility layer
2014-09-17, by blanchet
avoid clash with Quickcheck's generated 'random_xxx' function
2014-09-17, by blanchet
added missing 'restore' in 'transfer' plugin
2014-09-17, by blanchet
syntactic check to determine when to prove 'nested_size_o_map'
2014-09-17, by blanchet
support (finite values of) codatatypes in Quickcheck
2014-09-17, by blanchet
tuned fact visibility
2014-09-16, by blanchet
register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-16, by blanchet
took out 'old_datatype' examples -- those just cause timeouts in Isatests
2014-09-16, by blanchet
added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-16, by blanchet
added lemma
2014-09-16, by nipkow
add target language evaluators for the value command;
2014-09-16, by Andreas Lochbihler
tuning
2014-09-15, by blanchet
refactoring
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
set 'mono' attribute on 'rel_mono'
2014-09-15, by blanchet
'code' is needed for extraction datatype
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
removed accidental '@{print}'
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
more hints on how to port 'size'
2014-09-15, by blanchet
tuned definition of 'size' function to get nicer properties
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
document size difference
2014-09-15, by blanchet
generate 'code' attribute only if 'code' plugin is enabled
2014-09-15, by blanchet
disable datatype 'plugins' for internal types
2014-09-14, by blanchet
ported Imperative HOL to new datatypes
2014-09-13, by blanchet
imported patch phantoms
2014-09-13, by blanchet
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
2014-09-12, by blanchet
new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead
2014-09-12, by blanchet
run larger nominal examples only 'ISABELLE_FULL_TEST'
2014-09-12, by blanchet
refactor repeated terms in a single variable
2014-09-12, by desharna
make 'ctr_transfer' tactic more robust
2014-09-12, by desharna
make 'rel_sel' and 'map_sel' tactics more robust
2014-09-12, by desharna
Changing the way the dependencies are managed.
2014-09-12, by fleury
correction in the thf0 parser ("(=)" found in a Satallax proof).
2014-09-12, by fleury
merge
2014-09-12, by blanchet
fixed spellings
2014-09-12, by blanchet
NEWS
2014-09-12, by haftmann
abstract product over monoid for lists
2014-09-11, by haftmann
use proto_base_sort uniformly
2014-09-11, by haftmann
fixed some spelling mistakes
2014-09-11, by blanchet
tuned comment
2014-09-11, by blanchet
more porting to new datatypes
2014-09-11, by blanchet
tuning terminology
2014-09-11, by blanchet
compile
2014-09-11, by blanchet
renamed example theory for consistency
2014-09-11, by blanchet
updated ROOT
2014-09-11, by blanchet
tuned documentation
2014-09-11, by blanchet
updated news
2014-09-11, by blanchet
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
2014-09-11, by blanchet
move datatype benchmarks
2014-09-11, by blanchet
use new datatypes for benchmarks
2014-09-11, by blanchet
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-11, by blanchet
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-11, by blanchet
tuning
2014-09-11, by blanchet
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
2014-09-11, by blanchet
tuning
2014-09-11, by blanchet
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
2014-09-11, by blanchet
speed up old Nominal by killing type variables
2014-09-11, by blanchet
took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
2014-09-11, by blanchet
more docs
2014-09-11, by blanchet
new deads go to the end
2014-09-11, by traytel
comment
2014-09-11, by blanchet
more material on lists
2014-09-10, by haftmann
explicit check phase to guide type inference of class expression towards one single type variable
2014-09-10, by haftmann
tuned
2014-09-10, by haftmann
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
2014-09-10, by haftmann
tuning
2014-09-09, by blanchet
proper checks -- the calls data structure may contain spurious entries
2014-09-09, by blanchet
avoid exception
2014-09-09, by blanchet
avoid internal fact
2014-09-09, by blanchet
restored old case names
2014-09-09, by blanchet
compile
2014-09-09, by blanchet
avoid duplicate case names
2014-09-09, by blanchet
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
2014-09-09, by blanchet
preserve case names in '(co)induct' theorems generated by prim(co)rec'
2014-09-09, by blanchet
hide DEADID/ID theorems
2014-09-09, by blanchet
tuning
2014-09-09, by blanchet
more canonical (and correct) local theory threading
2014-09-09, by blanchet
removed 'datatype_compat's that are no longer needed
2014-09-09, by blanchet
documented extraction plugin
2014-09-09, by blanchet
made realizer more robust in the face of nesting through functions
2014-09-09, by blanchet
removed debugging junk
2014-09-09, by blanchet
renamed ML file and module
2014-09-09, by blanchet
made datatype realizer plugin work for new-style datatypes with no nesting
2014-09-09, by blanchet
ported HOL-Proofs-Lambda to new datatypes
2014-09-09, by blanchet
ported HOL-Proofs-Extraction to new datatypes
2014-09-09, by blanchet
made SML/NJ happier
2014-09-09, by blanchet
more porting to new datatypes
2014-09-09, by blanchet
tuned IArray code generator w.r.t. map rel set
2014-09-09, by blanchet
ported Nitpick_Examples to new datatypes
2014-09-09, by blanchet
set 'fundef_cong' attribute also for (co)datatypes with no live type variables
2014-09-09, by blanchet
ported IArray to new datatypes
2014-09-09, by blanchet
prevent infinite loop when type variables are of a non-'type' sort
2014-09-09, by blanchet
tuned code
2014-09-09, by blanchet
ported MicroJava to new datatypes
2014-09-09, by blanchet
rename_tac'd scrips
2014-09-09, by blanchet
ported Unix to new datatypes
2014-09-09, by blanchet
ported Isar_Examples to new datatypes
2014-09-09, by blanchet
ported Decision_Procs to new datatypes
2014-09-09, by blanchet
ported Induct to new datatypes
2014-09-09, by blanchet
half-ported Imperative HOL to new datatypes
2014-09-09, by blanchet
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-09, by blanchet
tuned messages
2014-09-09, by blanchet
rename_tac'd scripts
2014-09-09, by blanchet
reverted 83a8570b44bc, which was a misunderstanding
2014-09-09, by blanchet
rename_tac'd script
2014-09-09, by blanchet
ported Bali to new datatypes
2014-09-09, by blanchet
rename_tac'd scripts
2014-09-09, by blanchet
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-09-09, by blanchet
merged
2014-09-09, by nipkow
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-09, by nipkow
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
2014-09-09, by steckerm
more docs
2014-09-08, by blanchet
more documentation
2014-09-08, by blanchet
made 'lifting' plugin more robust
2014-09-08, by blanchet
tuned command descriptions
2014-09-08, by blanchet
generate better internal names, with name of the target type in it
2014-09-08, by blanchet
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
2014-09-08, by blanchet
added flag to 'typedef' to allow concealed definitions
2014-09-08, by blanchet
ported old Nominal to use new datatypes
2014-09-08, by blanchet
made tactic even more robust w.r.t. dead variables
2014-09-08, by traytel
made N2M work with sort constraints (cf. TODO)
2014-09-08, by blanchet
compile
2014-09-08, by blanchet
honour sorts in N2M
2014-09-08, by blanchet
proper sort constraints in map and rel theorems
2014-09-08, by blanchet
made new countable tactic work with sorts other than 'type'
2014-09-08, by blanchet
adapted examples to latest changes
2014-09-08, by blanchet
made code work also in the presence of deads
2014-09-08, by blanchet
export right sorts
2014-09-08, by blanchet
test sorts
2014-09-08, by blanchet
use right sort constraints
2014-09-08, by blanchet
never include hidden names -- these cannot be referenced afterward
2014-09-08, by blanchet
use compatibility layer
2014-09-08, by blanchet
made SML/NJ happire
2014-09-08, by blanchet
export useful functions for users of (co)recursors
2014-09-08, by blanchet
improved caching
2014-09-08, by blanchet
compile
2014-09-08, by blanchet
wildcards in plugins
2014-09-08, by blanchet
improved 'datatype_compat' further for recursion through functions
2014-09-08, by blanchet
no type-based lookup -- these fail in the general, ambiguous case
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
more examples/tests
2014-09-08, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip