isabelle: Graph

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
prevent pretty printer from automatically annotating numerals
2013-05-22, by smolkas
tuned
2013-05-22, by smolkas
simplified example and proof
2013-05-22, by nipkow
tuned
2013-05-22, by nipkow
tuned messages;
2013-05-21, by wenzelm
proper options;
2013-05-21, by wenzelm
proper options;
2013-05-21, by wenzelm
more markup;
2013-05-21, by wenzelm
tuned;
2013-05-21, by wenzelm
less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
2013-05-21, by wenzelm
proper context;
2013-05-21, by wenzelm
make SML/NJ happy;
2013-05-21, by wenzelm
added CASC-related files, to keep a public record of the Isabelle submission at the competition
2013-05-21, by blanchet
disabled choice in Satallax
2013-05-21, by blanchet
use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages
2013-05-21, by blanchet
prefer compiled version of LEO-II and Satallax if available
2013-05-21, by blanchet
updated remote provers
2013-05-21, by blanchet
added compatibility alias
2013-05-21, by blanchet
merged
2013-05-20, by wenzelm
more rigorous check of simplifier context;
2013-05-20, by wenzelm
proper context;
2013-05-20, by wenzelm
proper context;
2013-05-20, by wenzelm
proper run-time context;
2013-05-20, by wenzelm
more precise treatment of theory vs. Proof.context;
2013-05-20, by wenzelm
proper run-time context;
2013-05-20, by wenzelm
tuned;
2013-05-20, by wenzelm
more explicit Session.update_options as source of Global_Options event;
2013-05-20, by wenzelm
even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);
2013-05-20, by wenzelm
tuned;
2013-05-20, by wenzelm
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-05-20, by wenzelm
reset options last -- other parts of the system may still need them;
2013-05-20, by wenzelm
tuned signature;
2013-05-20, by wenzelm
updated Sledgehammer docs
2013-05-20, by blanchet
parse agsyHOL proofs (as unsat cores)
2013-05-20, by blanchet
freeze types in Sledgehammer goal, not just terms
2013-05-20, by blanchet
generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
2013-05-20, by blanchet
tuned code
2013-05-20, by blanchet
started adding agsyHOL as an experimental prover
2013-05-20, by blanchet
defined lvars and rvars of commands separately.
2013-05-20, by nipkow