isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

adapted example (cf. 78a3d5006cf1)
2013-06-07, by blanchet
code simplifications (cf. 78a3d5006cf1)
2013-06-07, by blanchet
killed dead code
2013-06-07, by blanchet
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
2013-06-07, by blanchet
killed dead code
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
tuned
2013-06-07, by nipkow
tuned variable names
2013-06-07, by nipkow
tuned
2013-06-07, by nipkow
tuning
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
[mq]: tuning
2013-06-07, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
fixed failure in coinduction rule tactic
2013-06-06, by blanchet
too much qualification is like too little
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
merge
2013-06-06, by blanchet
tuning
2013-06-06, by blanchet
tuned defs
2013-06-06, by nipkow
avoid duplicate call to "mk_fold_rec_args_types" function
2013-06-06, by blanchet
continuation of f461dca57c66
2013-06-06, by blanchet
renamed ML variables
2013-06-06, by blanchet
tuned record field names to avoid confusion between low-level and high-level constants/theorems
2013-06-06, by blanchet
tuned signature
2013-06-06, by blanchet
support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)
2013-06-06, by blanchet
tuned ML variable names
2013-06-06, by blanchet
transfer rule for listsum
2013-06-05, by kuncar
more reflexivity rules (for OO)
2013-06-05, by kuncar
tuning
2013-06-05, by blanchet
avoid code duplication
2013-06-05, by blanchet
eliminated dead argument
2013-06-05, by blanchet
one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
simpler, more robust iterator goal construction code
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
reverted 23929f647f79 -- not needed after all
2013-06-05, by blanchet
killed dead code
2013-06-05, by blanchet
tuning
2013-06-05, by blanchet
slightly nicer ML interface
2013-06-05, by blanchet
added convenience function
2013-06-05, by blanchet
keep a record of the fixpoint equations
2013-06-05, by blanchet
export ML function (needed for "primrec_new")
2013-06-05, by blanchet
export ML function
2013-06-04, by blanchet
corrected name
2013-06-03, by nipkow
tuned proofs
2013-06-03, by nipkow
type class for confined subtraction
2013-06-02, by haftmann
denesting of functions
2013-06-02, by haftmann
some meagure hints concerning reification
2013-06-02, by haftmann
make reification part of HOL
2013-06-02, by haftmann
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
2013-06-01, by wenzelm
Type_Annotation only works *after* uncheck (which usually requires authentic type information);
2013-06-01, by wenzelm
updated isatest stats;
2013-06-01, by wenzelm
tuned theory name
2013-06-01, by nipkow
tuned rules
2013-06-01, by nipkow
tuning
2013-05-31, by blanchet
renamed util function
2013-05-31, by blanchet
tuned;
2013-05-31, by wenzelm
make SML/NJ partially happy;
2013-05-31, by wenzelm
reflection without evaluation
2013-05-31, by haftmann
decomposed reflection steps into conversions;
2013-05-31, by haftmann
permit multiple variable arguments in reflect
2013-05-31, by haftmann
tuned
2013-05-31, by haftmann
dropped vacuous prefix
2013-05-31, by haftmann
combinator fold_range, corresponding to map_range
2013-05-31, by haftmann
merged
2013-05-31, by nipkow
more VC -> VCG
2013-05-31, by nipkow
VCG is standard name
2013-05-31, by nipkow
used nice syntax, removed lemma because it makes a nice exercise.
2013-05-31, by nipkow
NEWS about Spec_Check
2013-05-31, by bulwahn
tuned headers;
2013-05-30, by wenzelm
tuned messages -- some attempts to observe Isabelle output channel semantics;
2013-05-30, by wenzelm
less verbosity -- do not print final ();
2013-05-30, by wenzelm
tuned -- dynamic ML context is updated incrementally (see also e7c47fe56fbd);
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
toplevel invocation via implicit ML compilation context;
2013-05-30, by wenzelm
more direct Context.setmp_thread_data for one-way passing of context;
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
do not open ML structures;
2013-05-30, by wenzelm
prefer separate 'ML_command' for parallel evaluation;
2013-05-30, by wenzelm
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
2013-05-30, by wenzelm
more conventional spelling and grammar;
2013-05-30, by wenzelm
minor tuning -- more linebreaks;
2013-05-30, by wenzelm
removed pointless comment -- NB: Isabelle output is message-oriented with implicit line-boundaries;
2013-05-30, by wenzelm
standardized aliases;
2013-05-30, by wenzelm
do not handle arbitrary exceptions;
2013-05-30, by wenzelm
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
2013-05-30, by bulwahn
merged
2013-05-30, by wenzelm
tuned signature;
2013-05-30, by wenzelm
tuned signature;
2013-05-30, by wenzelm
misc tuning;
2013-05-30, by wenzelm
prefer existing beta_eta_conversion;
2013-05-30, by wenzelm
more standard fold/fold_rev;
2013-05-30, by wenzelm
tuned import;
2013-05-30, by wenzelm
misc tuning;
2013-05-30, by wenzelm
prefer existing beta_eta_conversion;
2013-05-30, by wenzelm
more standard names;
2013-05-30, by wenzelm
simplified method setup;
2013-05-30, by wenzelm
tuned -- prefer terminology of tactic / goal state;
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
misc tuning;
2013-05-30, by wenzelm
tuned;
2013-05-30, by wenzelm
tuned signature;
2013-05-30, by wenzelm
stay within regular tactic language -- avoid operating on whole proof state;
2013-05-30, by wenzelm