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 tip

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

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

isabelle