isabelle: Graph

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
standardized aliases;
2013-05-30, by wenzelm
space between minus sign and number for large negative number literals causes NumberFormatException at run-time
2013-05-30, by Andreas Lochbihler
tuned
2013-05-30, by nipkow
relational version of HoareT
2013-05-30, by kleing
obsolete;
2013-05-29, by wenzelm
resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
2013-05-29, by wenzelm
more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
2013-05-29, by wenzelm
tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-29, by wenzelm
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
2013-05-29, by wenzelm
tuned signature;
2013-05-29, by wenzelm
backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
2013-05-29, by wenzelm
observe type annotations in print translations as well, notably type_constraint_tr';
2013-05-29, by wenzelm
make SML/NJ happy;
2013-05-29, by wenzelm
tuning
2013-05-29, by blanchet
more work on general recursors
2013-05-29, by blanchet
tuning (use lists rather than pairs of lists throughout)
2013-05-29, by blanchet
generalized recursors, effectively reverting inductive half of c7a034d01936
2013-05-29, by blanchet
tuning
2013-05-29, by blanchet
merged
2013-05-28, by wenzelm
explicit support for type annotations within printed syntax trees;
2013-05-28, by wenzelm
more explicit Printer.type_emphasis, depending on show_type_emphasis;
2013-05-28, by wenzelm
tuning (refactoring)
2013-05-28, by blanchet
refactored triplicated functionality
2013-05-28, by blanchet
tuning -- avoided unreadable true/false all over the place for LFP/GFP
2013-05-28, by blanchet
merge
2013-05-28, by blanchet
don't create needless constant
2013-05-28, by blanchet
merged
2013-05-28, by popescua
fixed broken Cardinals and BNF due to Order_Union
2013-05-28, by popescua
no confusing special behavior in debug mode
2013-05-28, by blanchet
tuned Nitpick message to be in sync with similar warning from Kodkod
2013-05-28, by blanchet
merged
2013-05-28, by popescua
merged Well_Order_Extension into Zorn
2013-05-28, by popescua
removed junk (cf. 667961fa6a60);
2013-05-28, by wenzelm
exported ML function
2013-05-28, by blanchet
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-28, by blanchet
clean up list of theorems
2013-05-28, by blanchet
removed needless comment (yes, sum_case_if is needed)
2013-05-28, by blanchet
tuned
2013-05-28, by nipkow
actually test theory Order_Union;
2013-05-27, by wenzelm
more direct notation;
2013-05-27, by wenzelm
merged
2013-05-27, by wenzelm
more literal tokens, e.g. "EX!";
2013-05-27, by wenzelm
report markup for ast translations;
2013-05-27, by wenzelm
tuned;
2013-05-27, by wenzelm
tuned;
2013-05-27, by wenzelm
discontinued obsolete show_all_types;
2013-05-27, by wenzelm
added Ordered_Union
2013-05-27, by popescua
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
2013-05-24, by popescua
well-order extension (by Christian Sternagel)
2013-05-24, by popescua
modernized Zorn (by Christian Sternagel)
2013-05-24, by popescua
merged
2013-05-27, by wenzelm
more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
2013-05-27, by wenzelm
instantiate types as well (see also Thm.first_order_match);
2013-05-27, by wenzelm
tuned;
2013-05-27, by wenzelm
updated to ProofGeneral-4.2;
2013-05-27, by wenzelm
uniform Term_Position.markers (cf. dbadb4d03cbc);
2013-05-27, by wenzelm
get rid of "show_all_types" in Nitpick
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
killed dead argument
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
generalized "mk_co_iter" to handle mutualized (co)iterators
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
tuned
2013-05-27, by nipkow
tuned
2013-05-27, by nipkow
merged
2013-05-27, by nipkow
tuned
2013-05-27, by nipkow
merged
2013-05-26, by wenzelm
position constraint for bound dummy -- more PIDE markup;
2013-05-26, by wenzelm
position constraint for dummy_pattern -- more PIDE markup;
2013-05-26, by wenzelm
tuned;
2013-05-26, by wenzelm
tuned signature;
2013-05-26, by wenzelm
tuned -- less ML compiler warnings;
2013-05-26, by wenzelm
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
2013-05-26, by wenzelm
more uniform context;
2013-05-26, by wenzelm
tuned signature;
2013-05-26, by wenzelm
more conventional pretty printing;
2013-05-26, by wenzelm
tuned white-space;
2013-05-26, by wenzelm
more specific structure for registration into theory and dependency onto locale
2013-05-26, by haftmann
examples for interpretation into target
2013-05-26, by haftmann
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
2013-05-26, by blanchet
handle lambda-lifted problems in Isar construction code
2013-05-26, by blanchet
simpler proof through custom summation function
2013-05-26, by nipkow
merged
2013-05-25, by wenzelm
tuned;
2013-05-25, by wenzelm
tuned;
2013-05-25, by wenzelm
tuned;
2013-05-25, by wenzelm
tuned;
2013-05-25, by wenzelm
syntax translations always depend on context;
2013-05-25, by wenzelm
updated keywords;
2013-05-25, by wenzelm
weaker precendence of syntax for big intersection and union on sets
2013-05-25, by haftmann
tuned structure
2013-05-25, by haftmann
add lemma
2013-05-25, by noschinl
bookkeeping and input syntax for exact specification of names of symbols in generated code
2013-05-24, by haftmann
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
2013-05-24, by haftmann
dedicated module for code symbol data
2013-05-24, by haftmann
symbol data covers class relations also
2013-05-24, by haftmann
merged
2013-05-24, by wenzelm
proper internal error, not user error;
2013-05-24, by wenzelm
tuned;
2013-05-24, by wenzelm
tuned signature;
2013-05-24, by wenzelm
tuned;
2013-05-24, by wenzelm
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
2013-05-24, by wenzelm
tuned signature -- slightly more general operations (cf. term.ML);
2013-05-24, by wenzelm
re-use Pattern.unify_types, including its trace_unify_fail option;
2013-05-24, by wenzelm
tuned signature;
2013-05-24, by wenzelm
improved handling of free variables' types in Isar proofs
2013-05-24, by blanchet
pass noninteractive flag -- necessary to run under CASC's "runsolver" program
2013-05-24, by blanchet
untabify
2013-05-24, by blanchet
more lemmas for sorted_list_of_set
2013-05-23, by noschinl
prefer object equality
2013-05-23, by kleing
slightly clearer formulation
2013-05-23, by kleing
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
2013-05-22, by haftmann
mark local theory as brittle also after interpretation inside locales;
2013-05-22, by haftmann
merged
2013-05-22, by wenzelm
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
2013-05-22, by wenzelm
tuned signature;
2013-05-22, by wenzelm
more informative Build.build_results;
2013-05-22, by wenzelm
stop protocol handlers as well;
2013-05-22, by wenzelm
more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
2013-05-22, by wenzelm
explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-05-22, by wenzelm