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

standardized alias;
2012-04-06, by wenzelm
fixed document;
2012-04-06, by wenzelm
merged
2012-04-06, by wenzelm
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
2012-04-06, by huffman
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
2012-04-05, by kuncar
make Quotient_Def.lift_raw_const working again
2012-04-05, by kuncar
use standard quotient lemmas to generate transfer rules
2012-04-05, by huffman
add transfer lemmas for quotients
2012-04-05, by huffman
define reflp directly, in the manner of symp and transp
2012-04-05, by huffman
set up and use lift_definition for word operations
2012-04-05, by huffman
lift_definition declares transfer_rule attribute
2012-04-05, by huffman
configure transfer method for 'a word -> int
2012-04-05, by huffman
added timestamps to logging of named thms
2012-04-05, by krauss
merged
2012-04-05, by huffman
merged
2012-04-04, by huffman
add lemmas for generating transfer rules for typedefs
2012-04-04, by huffman
tuned;
2012-04-05, by sultana
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
2012-04-04, by sultana
merge
2012-04-04, by Cezary Kaliszyk
HOL/Import more precise map types
2012-04-04, by Cezary Kaliszyk
HOL/Import typed matches against Isabelle typedef result
2012-04-04, by Cezary Kaliszyk
connect the Quotient package to the Lifting package
2012-04-04, by kuncar
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04, by kuncar
tuned;
2012-04-04, by sultana
added interpretation for formula conditional;
2012-04-04, by sultana
refactored tptp lex;
2012-04-04, by sultana
refactored tptp yacc to bring close to official spec;
2012-04-04, by sultana
transfer method generalizes over free variables in goal
2012-04-04, by huffman
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-04, by huffman
update keywords file
2012-04-04, by huffman
merged
2012-04-04, by huffman
fix typos
2012-04-04, by huffman
lift_definition command generates transfer rule
2012-04-04, by huffman
prove_quot_theorem fixes types
2012-04-04, by huffman
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
2012-04-04, by bulwahn
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
2012-04-04, by bulwahn
stop node execution at first unassigned exec;
2012-04-06, by wenzelm
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-06, by wenzelm
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
2012-04-05, by wenzelm
less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05, by wenzelm
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05, by wenzelm
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
2012-04-05, by wenzelm
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

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

isabelle