2016-03-29 blanchet 2016-03-29 added sketchy 'corec' documentation
2016-03-28 blanchet 2016-03-28 compile
2016-03-28 blanchet 2016-03-28 updated Sledgehammer documentation
2016-03-28 blanchet 2016-03-28 a more generous hard timeout
2016-03-28 blanchet 2016-03-28 early warning when Sledgehammer finds a proof
2016-03-28 blanchet 2016-03-28 another 'corec' example
2016-03-28 blanchet 2016-03-28 don't ask too much of 'transfer_prover'
2016-03-28 blanchet 2016-03-28 commented out for now
2016-03-28 blanchet 2016-03-28 tuning
2016-03-28 blanchet 2016-03-28 FIXME
2016-03-28 blanchet 2016-03-28 avoid 'prove_sorry' for unreliable tactics
2016-03-28 blanchet 2016-03-28 reused code
2016-03-28 blanchet 2016-03-28 tuning
2016-03-28 blanchet 2016-03-28 tuned examples
2016-03-28 blanchet 2016-03-28 new 'corec' example
2016-03-28 blanchet 2016-03-28 more reliable check for rhs variables
2016-03-28 blanchet 2016-03-28 strengthened tactic
2016-03-28 blanchet 2016-03-28 generalized ML function
2016-03-28 blanchet 2016-03-28 added '_legacy' suffixes
2016-03-28 blanchet 2016-03-28 generalized ML interface
2016-03-28 blanchet 2016-03-28 tuning
2016-03-28 blanchet 2016-03-28 refined experimental option of Sledgehammer
2016-03-26 wenzelm 2016-03-26 tuned;
2016-03-26 wenzelm 2016-03-26 explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-26 wenzelm 2016-03-26 obsolete -- done in Isabelle_Process.init_options;
2016-03-26 wenzelm 2016-03-26 clarified use of options;
2016-03-26 wenzelm 2016-03-26 tuned signature;
2016-03-26 wenzelm 2016-03-26 clarified use of options;
2016-03-26 wenzelm 2016-03-26 avoid hardwired values;
2016-03-26 wenzelm 2016-03-26 eliminated duplicate;
2016-03-26 wenzelm 2016-03-26 more operations;
2016-03-24 nipkow 2016-03-24 merged
2016-03-24 nipkow 2016-03-24 merged
2016-03-24 nipkow 2016-03-24 added Leftist_Heap
2016-03-24 wenzelm 2016-03-24 updated to scala-2.11.8;
2016-03-24 wenzelm 2016-03-24 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
2016-03-24 wenzelm 2016-03-24 more operations;
2016-03-24 wenzelm 2016-03-24 tuned signature;
2016-03-23 kleing 2016-03-23 HOL-Word: add stronger bl_to_bin_lt2p_drop
2016-03-23 blanchet 2016-03-23 proper sectioning
2016-03-23 blanchet 2016-03-23 sorted out type issue with sort constraints
2016-03-22 blanchet 2016-03-22 tuned whitespace
2016-03-22 blanchet 2016-03-22 compile
2016-03-22 blanchet 2016-03-22 added 'corec' examples and tests
2016-03-22 blanchet 2016-03-22 file header
2016-03-22 blanchet 2016-03-22 added two 'corec' examples
2016-03-22 blanchet 2016-03-22 document addition of 'corec'
2016-03-22 blanchet 2016-03-22 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-22 blanchet 2016-03-22 put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-03-22 blanchet 2016-03-22 nicer error
2016-03-22 blanchet 2016-03-22 more debugging
2016-03-22 blanchet 2016-03-22 more general, reliable N2M
2016-03-22 blanchet 2016-03-22 better warning, with definitions in right order
2016-03-22 blanchet 2016-03-22 export ML function
2016-03-22 blanchet 2016-03-22 added timers to N2M
2016-03-22 traytel 2016-03-22 document that n2m does not depend on most things in fp_sugar in its type
2016-03-21 wenzelm 2016-03-21 clarified rule structure;
2016-03-21 wenzelm 2016-03-21 accomodate Isabelle identifiers with subscripts;
2016-03-21 wenzelm 2016-03-21 more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
2016-03-21 wenzelm 2016-03-21 eliminated unused argument (see also 58110c1e02bc);