isabelle: Graph

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
tuned docs
2014-09-08, by blanchet
properly note theorems for split recursors
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
updated docs
2014-09-08, by blanchet
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
export one more ML function
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
more compatibility documentation
2014-09-08, by blanchet
refactored MaSh files to avoid regenerating exports on each eval
2014-09-08, by blanchet
added missing 'transpose'
2014-09-08, by blanchet
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
2014-09-08, by blanchet
made tactic more robust w.r.t. dead variables
2014-09-08, by traytel
restrictive options for class dependencies
2014-09-07, by haftmann
separated class_deps command into separate file
2014-09-07, by haftmann
Added translation for lambda expressions in terms.
2014-09-07, by steckerm
explicit theory with additional, less commonly used list operations
2014-09-07, by haftmann
generalized
2014-09-07, by haftmann
theory about sum and product on function bodies
2014-09-06, by haftmann
theory about lexicographic ordering on functions
2014-09-06, by haftmann
added various facts
2014-09-06, by haftmann
Generalised card_length_listsum to all m
2014-09-05, by paulson
added lemma
2014-09-05, by nipkow
updated docs
2014-09-05, by blanchet
pretend code generation is a ctr_sugar plugin
2014-09-05, by blanchet
updated docs
2014-09-05, by blanchet
added 'plugins' option to control which hooks are enabled
2014-09-05, by blanchet
introduced mechanism to filter interpretations
2014-09-05, by blanchet
fixed infinite loops in 'register' functions + more uniform API
2014-09-05, by blanchet
named interpretations
2014-09-05, by blanchet
centralized and cleaned up naming handling
2014-09-05, by blanchet
cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-09-04, by hoelzl
tuned Nitpick and Refute examples, which are too slow on some testing machines
2014-09-04, by blanchet
tweaked setup for datatype realizer
2014-09-04, by blanchet
renamed internal constant
2014-09-04, by blanchet
moved code around
2014-09-04, by blanchet
tuned size function generation
2014-09-04, by blanchet
tuning
2014-09-04, by blanchet
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-09-03, by blanchet
tuned ctr_sugar database handling
2014-09-03, by blanchet
tuned BNF database handling
2014-09-03, by blanchet
intelligible errors instead of tactic failures
2014-09-03, by blanchet
reenabled yet another example
2014-09-03, by blanchet
made new tactic even more robust
2014-09-03, by blanchet
reenabled more examples
2014-09-03, by blanchet
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
2014-09-03, by blanchet
reintroduced more examples
2014-09-03, by blanchet
improved tactic further
2014-09-03, by blanchet
reenabled example
2014-09-03, by blanchet
improved new countability tactic
2014-09-03, by blanchet
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
2014-09-03, by blanchet
more robust exception handling
2014-09-03, by blanchet
added tests for new 'countable_datatype' proof method
2014-09-03, by blanchet
lessen the burden on the caller: sort where necessary in n2m
2014-09-03, by traytel
added compatibility function
2014-09-03, by blanchet
added countable tactic for new-style datatypes
2014-09-03, by blanchet
tuning
2014-09-03, by blanchet
registered 'typerep' as countable again
2014-09-03, by blanchet
moved old datatype material around
2014-09-03, by blanchet
removed vacuous theorem references
2014-09-03, by blanchet
commented out failing tactic (now that 'typerep' is defined using the new package
2014-09-03, by blanchet
tuned imports
2014-09-03, by blanchet
use 'datatype_new'
2014-09-03, by blanchet
use 'datatype_new' in 'Main'
2014-09-03, by blanchet
take out 'x = C' of the simplifier for unit types
2014-09-03, by blanchet
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
2014-09-03, by blanchet
ported 'Statespace' to support new datatypes as well
2014-09-03, by blanchet
use 'datatype_new' in Quickcheck examples
2014-09-03, by blanchet
more compatibility functions
2014-09-03, by blanchet
codatatypes are not datatypes
2014-09-03, by blanchet
ported Quickcheck to support new datatypes better
2014-09-03, by blanchet
removed more slow Refute tests
2014-09-02, by blanchet
tuned Refute example
2014-09-02, by blanchet
Some work on the new waldmeister integration
2014-09-02, by steckerm
merged
2014-09-02, by boehmes
replay Z3 rewrite steps that lift if-then-else expressions
2014-09-02, by boehmes
test discriminators/selectors in BNF regression suite
2014-09-02, by traytel
merge
2014-09-02, by blanchet
made SML/NJ happier
2014-09-02, by blanchet
tuning
2014-09-02, by blanchet
silenced nonexhaustive primrec warnings
2014-09-02, by traytel
more convenient printing of real numbers after evaluation
2014-09-02, by haftmann
avoid more 'bad background theory' issues
2014-09-01, by blanchet
ported TFL to mixture of old and new datatypes
2014-09-01, by blanchet
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
2014-09-01, by blanchet
ported to use new-style datatypes
2014-09-01, by blanchet
ported Refute to use new datatypes when possible
2014-09-01, by blanchet
renamed BNF theories
2014-09-01, by blanchet
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
2014-09-01, by blanchet
added primrec compatibility function
2014-09-01, by blanchet
more work on compatibility interfaces
2014-09-01, by blanchet
added compatibility examples/tests
2014-09-01, by blanchet
implemented compatibility definition of datatype
2014-09-01, by blanchet
implemented compatibility interpretation
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
more compatibility between old- and new-style datatypes
2014-09-01, by blanchet
added theory-based getters for convenience
2014-09-01, by blanchet
made transfer functions slightly more general
2014-09-01, by blanchet
tuned signatures
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01, by blanchet
tuned structure inclusion
2014-09-01, by blanchet
took out legacy material from 'HOL/Library/Library.thy'
2014-09-01, by blanchet
removed commented out parts
2014-09-01, by blanchet
tuned whitespace
2014-09-01, by blanchet
document 'set_transfer'
2014-09-01, by desharna
generate 'set_transfer' for BNFs
2014-09-01, by desharna
document 'rel_transfer'
2014-09-01, by desharna
generate 'rel_transfer' for BNFs
2014-09-01, by desharna
document 'map_transfer'
2014-09-01, by desharna
note 'map_transfer' more often
2014-09-01, by desharna
separated listsum material
2014-08-31, by haftmann
restored generic value slot, retaining default behaviour and separate approximate command
2014-08-31, by haftmann
convenient printing of (- 1 :: integer) after code evaluation
2014-08-31, by haftmann
inlined unused definition
2014-08-30, by haftmann
add simp rules for divisions of numerals in floor and ceiling.
2014-08-29, by hoelzl
document 'disc_transfer'
2014-08-29, by desharna
generate 'disc_transfer' for (co)datatypes
2014-08-29, by desharna
document 'case_transfer'
2014-08-29, by desharna
generate 'case_transfer' for (co)datatypes
2014-08-29, by desharna
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28, by blanchet
reworked unskolemization for SPASS
2014-08-28, by blanchet
clarified docs
2014-08-28, by blanchet
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
2014-08-28, by blanchet
prefer '0.2 ms' to '249 \<mu>s'
2014-08-28, by blanchet
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
2014-08-28, by blanchet
fixed second computations
2014-08-28, by blanchet
merged minimize and auto_minimize
2014-08-28, by blanchet
pass options to remote Vampire
2014-08-28, by blanchet
removed show stuttering
2014-08-28, by blanchet
generate 'thesis' variable in Sledgehammer Isar proofs
2014-08-28, by blanchet
show microseconds as well (useful when playing with Isar proofs)
2014-08-28, by blanchet
tuned message
2014-08-28, by blanchet
made trace more informative when minimization is enabled
2014-08-28, by blanchet
took out one more occurrence of 'PolyML.makestring'
2014-08-28, by blanchet
try 'skolem' method first for Z3
2014-08-28, by blanchet
tuned tracing output (indirectly)
2014-08-28, by blanchet
going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
2014-08-28, by blanchet
moved skolem method
2014-08-28, by blanchet
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28, by blanchet
tuned method description
2014-08-28, by blanchet
three-line 'obtain' format for generated Isar proofs
2014-08-28, by blanchet
tuned;
2014-08-28, by wenzelm
more liberal embedded "text", which includes cartouches;
2014-08-28, by wenzelm
intern xthm only once;
2014-08-28, by wenzelm
tuned terminology
2014-08-28, by blanchet
moved new para to right section of NEWS
2014-08-28, by blanchet
minor NEWS fix
2014-08-28, by blanchet
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
2014-08-28, by blanchet
added 'OLD_' prefix in front of old solvers
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
prefixed all old SMT commands, attributes, etc., with 'old_'
2014-08-28, by blanchet
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
2014-08-28, by blanchet
renaming theory 'Old_SMT'
2014-08-28, by blanchet
moved old setup for SMT out
2014-08-28, by blanchet
moved old 'smt' method out of 'Main'
2014-08-28, by blanchet
reintroduced two-line-per-inference Isar proof format
2014-08-28, by blanchet
removed needless, and for (newer versions of?) Haskell problematic code equations
2014-08-28, by blanchet
removed obsolete RC tags;
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
Added tag Isabelle2014 for changeset 8f4a332500e4
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
more explicit Method.modifier with reported position;
2014-08-27, by wenzelm
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
2014-08-27, by wenzelm
added ML antiquotation @{source} for Symbol_Pos.source;
2014-08-27, by wenzelm
tuned signature;
2014-08-25, by wenzelm
removed not so interesting 'set_empty'
2014-08-27, by blanchet