isabelle: Graph

Added parantheses to code_type for heap monad
2013-06-18, by lammich
improved defs and proofs
2013-06-18, by nipkow
use \<^isub> in determ proof for display in book
2013-06-17, by kleing
merged
2013-06-17, by krauss
export dom predicate in the info record
2013-06-16, by krauss
export cases rule in the info record
2013-06-16, by krauss
made proofs more readable
2013-06-17, by nipkow
pragmatic executability for instance real :: open
2013-06-15, by haftmann
lifting for primitive definitions;
2013-06-15, by haftmann
selection operator smallest_prime_beyond
2013-06-15, by haftmann
documentation on code_printing and code_identifier
2013-06-15, by haftmann
more consistent parsing and reading of classes and type constructors
2013-06-15, by haftmann
another example lemma
2013-06-14, by kleing
store more theorems in data structure
2013-06-13, by blanchet
tuning
2013-06-13, by blanchet
simplified proofs
2013-06-13, by nipkow
prefer xsymbol for book
2013-06-12, by kleing
same order of properties as in While rule
2013-06-12, by nipkow
some comments on syntax and automation setup
2013-06-11, by kleing
uncheck terms before annotation to avoid awkward syntax
2013-06-11, by smolkas
tuning
2013-06-11, by blanchet
tuning
2013-06-11, by blanchet
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-06-11, by smolkas
reflexive nbe equation for equality on String.literal
2013-06-11, by haftmann
tuned whitespace
2013-06-10, by haftmann
dropped relics of ancient binary numeral case study
2013-06-10, by haftmann
merged
2013-06-10, by nipkow
all headings in upper case
2013-06-10, by nipkow
more int/nat transfer rules; examples of new untransferred attribute
2013-06-10, by huffman
more transfer rules for sets
2013-06-10, by huffman
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
2013-06-10, by huffman
use right context when exporting variables (cf. AFP Coinductive_List failures)
2013-06-10, by blanchet
keep track of nested BNFs
2013-06-10, by blanchet
tuning
2013-06-10, by blanchet
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
2013-06-08, by huffman
SPASS has more Uppercase keywords than I was fearing -- better always append _
2013-06-07, by blanchet
merge
2013-06-07, by blanchet
tuning
2013-06-07, by blanchet
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