isabelle: Graph

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
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
made "completish" mode a bit more complete
2013-05-19, by blanchet
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
2013-05-19, by haftmann
tuned and clarified
2013-05-19, by haftmann
tuned, including signature
2013-05-19, by haftmann
discontinued odd workaround for scala-2.10.0-RC1;
2013-05-18, by wenzelm
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-05-18, by wenzelm
explicit notion of public options, which are shown in the editor options dialog;
2013-05-18, by wenzelm
back to more paranoid interrupt test after request is cancelled -- avoid race condition;
2013-05-17, by wenzelm
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
2013-05-17, by wenzelm
added isabelle tty option -o;
2013-05-17, by wenzelm
oops;
2013-05-17, by wenzelm
renamed 'print_configs' to 'print_options';
2013-05-17, by wenzelm
proper option quick_and_dirty;
2013-05-17, by wenzelm
retain quick_and_dirty as-is -- no censorship;
2013-05-17, by wenzelm
more system-atic options;
2013-05-17, by wenzelm
added isabelle-process option -o;
2013-05-17, by wenzelm
more precise "eval", cf. isabelle build;
2013-05-17, by wenzelm
discontinued obsolete isabelle-process options -f and -u;
2013-05-17, by wenzelm
NEWS;
2013-05-17, by wenzelm
discontinued obsolete isabelle usedir, mkdir, make;
2013-05-17, by wenzelm
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
2013-05-17, by wenzelm
event timer as separate service thread;
2013-05-17, by wenzelm
tuned signature;
2013-05-17, by wenzelm
tuned signature -- emphasize thread creation here;
2013-05-17, by wenzelm
repair after bc01725d7918;
2013-05-17, by wenzelm
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
2013-05-17, by nipkow
tuned
2013-05-17, by nipkow
merged
2013-05-16, by wenzelm
more system options as context-sensitive config options;
2013-05-16, by wenzelm
Thy_Output.modes as proper option;
2013-05-16, by wenzelm
some system options as context-sensitive config options;
2013-05-16, by wenzelm
system options as context-sensitive configuration options within the attribute name space;
2013-05-16, by wenzelm
tuned signature;
2013-05-16, by wenzelm
properly handle SPASS constructors w.r.t. partially applied functions
2013-05-16, by blanchet
tuned signature -- depend on context by default;
2013-05-16, by wenzelm
reflexivity rules for the function type and equality
2013-05-16, by kuncar
tuned comments
2013-05-16, by blanchet
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
more work on SPASS datatypes
2013-05-16, by blanchet
tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-16, by blanchet
compile
2013-05-16, by blanchet
don't recognize overloaded constants as constructors for the purpose of removing type arguments
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
reintroduced syntax for "nonexhaustive" datatypes
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
more work on SPASS datatypes
2013-05-16, by blanchet
merged
2013-05-16, by Andreas Lochbihler
setup for set membership as a predicate for code_pred
2013-05-16, by Andreas Lochbihler
tuned
2013-05-16, by nipkow
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
2013-05-16, by kleing
merged
2013-05-16, by nipkow
finally: acom with pointwise access and update of annotations
2013-05-16, by nipkow
merged;
2013-05-15, by wenzelm
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
2013-05-15, by wenzelm
simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);
2013-05-15, by wenzelm
back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;
2013-05-15, by wenzelm
more standard Isabelle/ML structures for global preferences;
2013-05-15, by wenzelm
more basic print mode "ProofGeneral" (again);
2013-05-15, by wenzelm
uniform welcome -- actually visible on startup via Output.urgent_message;
2013-05-15, by wenzelm
more elementary ProofGeneral.thm_deps;
2013-05-15, by wenzelm
tuned;
2013-05-15, by wenzelm
moved files;
2013-05-15, by wenzelm
clarified default for Proofterm.proofs, according to etc/options and innermost setmp;
2013-05-15, by wenzelm
maintain ProofGeneral preferences within ProofGeneral module;
2013-05-15, by wenzelm
just one ProofGeneral module;
2013-05-15, by wenzelm
tuning
2013-05-15, by blanchet
more work on SPASS datatypes
2013-05-15, by blanchet
tuning
2013-05-15, by blanchet
no need to reinvent the wheel ("fold_map")
2013-05-15, by blanchet
more work on implementing datatype output for new SPASS
2013-05-15, by blanchet
tuned code
2013-05-15, by blanchet
compile
2013-05-15, by blanchet
renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-15, by blanchet
added datatype declaration syntax for next-gen SPASS
2013-05-15, by blanchet
abstract equalities only in a correspondence relation in a transfer domain rule
2013-05-15, by kuncar
superfluous transfer rule
2013-05-15, by kuncar
stronger reflexivity prover
2013-05-15, by kuncar
simplified modules and exceptions;
2013-05-14, by wenzelm
more elementary pgiptype;
2013-05-14, by wenzelm
prefer Markup.parse/print operations -- slight change of exception behaviour;
2013-05-14, by wenzelm
more uniform Markup.print_real;
2013-05-14, by wenzelm
removed dead code;
2013-05-14, by wenzelm
more uniform Markup.parse_real;
2013-05-14, by wenzelm
tuned signature;
2013-05-14, by wenzelm
more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;
2013-05-14, by wenzelm
tuned;
2013-05-14, by wenzelm
misc tuning and simplification;
2013-05-14, by wenzelm
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
2013-05-14, by wenzelm
more scalable File.write via separate chunks;
2013-05-14, by wenzelm
more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
2013-05-14, by wenzelm
support for more informative crashes;
2013-05-14, by wenzelm
more antiquotations;
2013-05-14, by wenzelm
tuned messages;
2013-05-14, by wenzelm
more generous java resources via ISABELLE_BUILD_JAVA_OPTIONS;
2013-05-14, by wenzelm
generate valid direct Isar proof also if the facts are contradictory
2013-05-14, by blanchet
tuned names
2013-05-14, by nipkow
tuned names
2013-05-14, by nipkow
removed obsolete PGIP material;
2013-05-13, by wenzelm
more direct output of remaining PGIP rudiments;
2013-05-13, by wenzelm
simplified preferences, removed obsolete operations;
2013-05-13, by wenzelm
tuned signature;
2013-05-13, by wenzelm
more direct output of remaining PGIP rudiments;
2013-05-13, by wenzelm
obsolete;
2013-05-13, by wenzelm
removed obsolete PGIP material;
2013-05-13, by wenzelm
recovered informative progress from 016cb7d8f297;
2013-05-13, by wenzelm
removed obsolete PGIP material;
2013-05-13, by wenzelm
clean startup of RAW session;
2013-05-13, by wenzelm
dummy PGIP id, which appears to be sufficient for PG/Emacs;
2013-05-13, by wenzelm
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
2013-05-13, by wenzelm
merged
2013-05-13, by wenzelm
option "goals_limit", with more uniform description;
2013-05-13, by wenzelm
clarified message when subgoals have been stripped -- unconditional;
2013-05-13, by wenzelm
retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-05-13, by wenzelm
typo
2013-05-13, by kuncar
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-05-13, by kuncar
try to detect assumptions of transfer rules that are in a shape of a transfer rule
2013-05-13, by kuncar
publish a private function
2013-05-13, by kuncar
tuned names
2013-05-13, by nipkow
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
2013-05-12, by wenzelm
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
2013-05-12, by wenzelm
prefer standard Isabelle/ML operations;
2013-05-12, by wenzelm
some system options as context-sensitive config options;
2013-05-12, by wenzelm
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
2013-05-12, by wenzelm
support for system options as context-sensitive config options;
2013-05-12, by wenzelm
tuned signature;
2013-05-12, by wenzelm
tuned comments;
2013-05-12, by wenzelm
support for options as preferences;
2013-05-12, by wenzelm
more operations in accordance to Scala version;
2013-05-12, by wenzelm
more systematic access to options default;
2013-05-12, by wenzelm
full default options for Isabelle_Process and Build;
2013-05-12, by wenzelm
decentralized historic settings;
2013-05-12, by wenzelm
removed obsolete test_markup;
2013-05-12, by wenzelm
Proof General interaction always uses Isar loop;
2013-05-12, by wenzelm
proper context;
2013-05-12, by wenzelm
merged
2013-05-11, by wenzelm
more direct PGIP/Emacs processing and output;
2013-05-11, by wenzelm
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
2013-05-11, by wenzelm
removed redundant modules;
2013-05-11, by wenzelm
removed some obsolete PGIP/PGEclipse material;
2013-05-11, by wenzelm
never open structure Unsynchronized (cf. "implementation" manual);
2013-05-11, by wenzelm
prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-05-11, by wenzelm
avoid PolyML.makestring, even in dead code;
2013-05-11, by wenzelm
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"
2013-05-11, by blanchet
don't apply an unnecessary morphism
2013-05-10, by kuncar
tuned
2013-05-10, by nipkow
relator coinduction for codatatypes
2013-05-09, by traytel
standard ivl notation [l,h]
2013-05-09, by nipkow
merged
2013-05-09, by nipkow
tuned
2013-05-08, by nipkow
avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time
2013-05-08, by blanchet
proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS
2013-05-08, by blanchet
use right default for "uncurried_aliases" with polymorphic SPASS
2013-05-08, by blanchet
relator induction for datatypes
2013-05-08, by traytel
store proper theorems even for fixed points that have no passive live variables
2013-05-08, by traytel
stronger monotonicity property for relators
2013-05-08, by traytel
make tactic actually work for op = as relator
2013-05-08, by traytel
tuned
2013-05-08, by nipkow
hide Fin on output
2013-05-08, by nipkow
removed dead argument
2013-05-07, by blanchet
more robust iterator construction (needed for mutualized FPs)
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
removed dead internal constants/theorems
2013-05-07, by traytel
removed tracing
2013-05-07, by blanchet
export one more function
2013-05-07, by blanchet
added field to record
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
removed dead code
2013-05-07, by blanchet
move function to library
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
more
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
code tuning
2013-05-07, by blanchet
merge
2013-05-07, by blanchet
refactoring
2013-05-07, by blanchet
export one more function + tuning
2013-05-07, by blanchet
do not unfold the definition of the relator as it is not defined in terms of srel anymore
2013-05-07, by traytel
tuned
2013-05-07, by traytel
got rid of the set based relator---use (binary) predicate based relator instead
2013-05-07, by traytel
tuned names + extended ML signature
2013-05-07, by blanchet
merged
2013-05-07, by nipkow
tuned name: filter -> constrain (longer but more intuitive)
2013-05-07, by nipkow
tuning
2013-05-07, by blanchet
imported patch refactor_coiter_constr
2013-05-07, by blanchet
tuned
2013-05-07, by nipkow
started factoring out coiter construction
2013-05-06, by blanchet
rationalize ML signature
2013-05-06, by blanchet
factor out construction of iterator
2013-05-06, by blanchet
tuning
2013-05-06, by blanchet
improved defns and proofs
2013-05-06, by nipkow
undo 46d911ab9170 since it causes problems
2013-05-06, by smolkas
allow '-'s in tptp ids to avoid problems with remote_vampire
2013-05-06, by smolkas
added preplay tracing
2013-05-06, by smolkas
handle dummy atp terms
2013-05-06, by smolkas
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
2013-05-06, by smolkas
added informative error messages
2013-05-06, by smolkas
tail recursive version of map, for code generation, optionally
2013-05-06, by nipkow
simplified proofs
2013-05-06, by nipkow
tuning
2013-05-03, by blanchet
pass certain readability-enhancing Vampire options only when an Isar proof is needed
2013-05-03, by blanchet
added lemma
2013-05-03, by nipkow
added lemma
2013-05-03, by nipkow
renamings
2013-05-02, by blanchet
code tuning
2013-05-02, by blanchet
signature tuning
2013-05-02, by blanchet
removed dead code
2013-05-02, by blanchet
tuned signature
2013-05-02, by blanchet
store (co)induction rules in data structure
2013-05-02, by blanchet
tuning names
2013-05-02, by blanchet
got rid of needless library function (find_minimum)
2013-05-02, by blanchet
one more lib function
2013-05-02, by blanchet
export one more function
2013-05-02, by blanchet
rationalized data structure
2013-05-02, by blanchet
added and moved library functions (used in primrec code)
2013-05-02, by blanchet
tuned names -- co_ and un_ with underscore are to be understood as (co) and (un)
2013-05-02, by blanchet
tuning
2013-05-02, by blanchet
more code rationalization
2013-05-02, by blanchet
more code rationalization
2013-05-02, by blanchet
more code rationalization
2013-05-02, by blanchet
refactoring
2013-05-02, by blanchet
tuned
2013-05-02, by nipkow
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
2013-05-01, by blanchet
tuned
2013-05-01, by nipkow
tuned
2013-05-01, by nipkow
tuning
2013-04-30, by blanchet
export more functions (useful for primrec_new)
2013-04-30, by blanchet
further enrich data structure
2013-04-30, by blanchet
more
2013-04-30, by blanchet
rationalized terminology (iterator = fold or rec, xxfoo = (co)foo or (un)foo)
2013-04-30, by blanchet
added fields to database
2013-04-30, by blanchet
tuned data structure
2013-04-30, by blanchet
renamed records
2013-04-30, by blanchet
added constructors to data structure
2013-04-30, by blanchet
added pre-BNFs to database
2013-04-30, by blanchet
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
2013-04-30, by blanchet
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
2013-04-30, by blanchet
Added maps, sets, rels to "simps" thm collection
2013-04-30, by blanchet
tuned
2013-04-30, by nipkow
comment tuning
2013-04-30, by blanchet
tuning
2013-04-30, by blanchet
tuning
2013-04-30, by blanchet
tuning
2013-04-30, by blanchet
signature tuning
2013-04-30, by blanchet
whitespace tuning
2013-04-30, by blanchet
tuned signature
2013-04-30, by blanchet
canonical names of classes
2013-04-30, by nipkow
merged
2013-04-29, by blanchet
register all (co)datatypes in local data
2013-04-29, by blanchet
create data structure for storing (co)datatype information
2013-04-29, by blanchet
avoid empty isabelletags.sty for the sake of arXiv;
2013-04-29, by wenzelm
merged
2013-04-29, by wenzelm
cygwin_root as optional argument;
2013-04-29, by wenzelm
use record instead of big tuple
2013-04-29, by blanchet
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
2013-04-29, by wenzelm
merge
2013-04-29, by blanchet
use base names, not full names
2013-04-29, by blanchet
tune signatures
2013-04-29, by blanchet
tuning
2013-04-29, by blanchet
tuning
2013-04-29, by blanchet
removed unreferenced thm
2013-04-29, by blanchet
tuned function signatures
2013-04-29, by blanchet
factored out derivation of coinduction, unfold, corec
2013-04-29, by blanchet
code tuning
2013-04-29, by blanchet
factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual
2013-04-29, by blanchet
tuned
2013-04-29, by nipkow
tuned operator precedence
2013-04-29, by traytel
use record instead of huge tuple
2013-04-29, by blanchet
renamed BNF "(co)data" commands to names that are closer to their final names
2013-04-29, by blanchet
tuned
2013-04-29, by nipkow
tuned
2013-04-29, by nipkow
tuned
2013-04-29, by nipkow
tuned
2013-04-28, by nipkow
Clarified confusing sentence in locales tutorial.
2013-04-27, by ballarin
uniform Proof.context for hyp_subst_tac;
2013-04-27, by wenzelm
tuned ML and thy file names
2013-04-27, by blanchet
merged
2013-04-26, by blanchet
for compatibility, generate recursor arguments in the same order as old package
2013-04-26, by blanchet
tuning in preparation for actual changes
2013-04-26, by blanchet
started working on compatibility with old package's recursor
2013-04-26, by blanchet
simplified def
2013-04-26, by nipkow
more standard argument order
2013-04-26, by nipkow
more intuitive syntax for equality-style discriminators of nullary constructors
2013-04-26, by blanchet
updated keywords
2013-04-26, by blanchet
put an underscore in prefix
2013-04-26, by blanchet
changed discriminator default: avoid mixing ctor and dtor views
2013-04-26, by blanchet
simplified def
2013-04-26, by nipkow
more standard order of arguments
2013-04-26, by nipkow
more funs
2013-04-26, by nipkow
simplified def
2013-04-26, by nipkow
removed unnecessary assumptions in some theorems about cardinal exponentiation
2013-04-25, by traytel
renamed "wrap_data" to "wrap_free_constructors"
2013-04-25, by blanchet
register coinductive type's coinduct rule
2013-04-25, by blanchet
compile
2013-04-25, by blanchet
adjusted stream library to coinduct attributes
2013-04-25, by blanchet
generate proper attributes for coinduction rules
2013-04-25, by blanchet
updated to jdk-7u21;
2013-04-25, by wenzelm
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25, by hoelzl
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-25, by hoelzl
spell conditional_ly_-complete lattices correct
2013-04-24, by hoelzl
specify nicer names for map, set and rel in the stream library
2013-04-25, by traytel
start making "wrap_data" more robust
2013-04-25, by blanchet
no eta-expansion for case in split rules and case_conv
2013-04-25, by blanchet
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
2013-04-25, by blanchet
proper error generated for wrong mixfix
2013-04-24, by blanchet
honor user-specified name for relator + generalize syntax
2013-04-24, by blanchet
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24, by blanchet
added "fundef_cong" attribute to "map_cong"
2013-04-24, by blanchet
optimized proofs
2013-04-24, by traytel
apply arguments to f and g in "case_cong"
2013-04-24, by blanchet
derive "map_cong"
2013-04-24, by blanchet
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
2013-04-24, by blanchet
killed dead code
2013-04-24, by blanchet
eta-contracted weak congruence rules (like in the old package)
2013-04-24, by blanchet
honor user-specified name for map function
2013-04-24, by blanchet
honor user-specified set function names
2013-04-24, by blanchet
parse set function name
2013-04-24, by blanchet
merged
2013-04-24, by nipkow
tuned
2013-04-24, by nipkow
took out workaround for bug fixed in 5af40820948b
2013-04-24, by traytel
merged
2013-04-24, by traytel
slightly more aggressive syntax translation for printing case expressions
2013-04-24, by traytel
avoid odd reinit after sublocale declaration
2013-04-24, by haftmann
moved defs into locale to reduce unnecessary polymorphism; tuned
2013-04-24, by nipkow
dropped dead code
2013-04-23, by haftmann
documentation and NEWS
2013-04-23, by haftmann
avoid accidental specialization of the types in the "map" property of codatatypes
2013-04-23, by blanchet
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
2013-04-23, by blanchet
more examples
2013-04-23, by blanchet
tuning
2013-04-23, by blanchet
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
2013-04-23, by blanchet
tuning
2013-04-23, by blanchet
tuned_comment
2013-04-23, by blanchet
(co)rec is (just as the (un)fold) the unique morphism;
2013-04-23, by traytel
tuned: unnamed contexts, interpretation and sublocale in locale target;
2013-04-23, by haftmann
target-sensitive user-level commands interpretation and sublocale
2013-04-23, by haftmann
ML interfaces for various kinds of interpretation
2013-04-23, by haftmann
brittleness stamping for local theories
2013-04-23, by haftmann
tuned
2013-04-23, by haftmann
removed type constraints
2013-04-22, by immler
NEWS
2013-04-22, by hoelzl
more sharing
2013-04-21, by haftmann
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
2013-04-21, by haftmann
dropped unusued identifier
2013-04-21, by haftmann
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
2013-04-21, by haftmann
tuned for uniformity
2013-04-21, by haftmann
reflection as official HOL tool
2013-04-21, by haftmann
follow Isabelle spacing praxis more thoroughly
2013-04-21, by haftmann
honour FIXMEs as far as feasible at the moment
2013-04-21, by haftmann
combined reify_data.ML into reflection.ML;
2013-04-21, by haftmann
proved termination for fun-based AI
2013-04-20, by nipkow
tuned
2013-04-20, by nipkow
tuned
2013-04-19, by nipkow
merged
2013-04-18, by wenzelm
tuned signature;
2013-04-18, by wenzelm
simplifier uses proper Proof.context instead of historic type simpset;
2013-04-18, by wenzelm
merged
2013-04-18, by nipkow
avoided map_of in def of fun_rep (but still needed for efficient code)
2013-04-18, by nipkow
spelling
2013-04-18, by haftmann
spelling
2013-04-18, by haftmann
tuned
2013-04-17, by nipkow
complete revision: finally got rid of annoying L-predicate
2013-04-17, by nipkow
moved leastness lemma
2013-04-17, by nipkow
proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
2013-04-16, by wenzelm
use automatic type coerctions in Sqrt example
2013-04-15, by hoelzl
make SML/NJ happy;
2013-04-15, by wenzelm
not all Nitpick 'constructors' are injective -- careful
2013-04-15, by blanchet
added another definition snipped
2013-04-14, by kleing
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
2013-04-12, by wenzelm
modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-12, by wenzelm
removed historic comments;
2013-04-12, by wenzelm
tuned exceptions -- avoid composing error messages in low-level situations;
2013-04-12, by wenzelm
tuned signature;
2013-04-12, by wenzelm
proper identifiers -- avoid crash of case translations;
2013-04-12, by wenzelm
reduced duplication
2013-04-12, by nipkow
do not add case translation syntax in rep_datatype compatibility mode
2013-04-11, by traytel
run type inference on input to wrap_data
2013-04-11, by traytel
installed case translations in BNF package
2013-04-11, by traytel
tuned
2013-04-11, by nipkow
more antiquotations;
2013-04-10, by wenzelm
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
2013-04-10, by wenzelm
updated keywords;
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
obsolete -- tools should refer to proper Proof.context;
2013-04-10, by wenzelm
discontinued obsolete ML antiquotation @{claset};
2013-04-10, by wenzelm
added ML antiquotation @{theory_context};
2013-04-10, by wenzelm
more standard module name Axclass (according to file name);
2013-04-10, by wenzelm
made SML/NJ happy
2013-04-10, by traytel
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2013-04-10, by hoelzl
NEWS and CONTRIBUTORS
2013-04-10, by traytel
declaration attribute for case combinators
2013-04-10, by traytel
Handle dummy patterns in parse translation rather than check phase
2013-04-09, by berghofe
disallow coercions to interfere with case translations
2013-04-06, by traytel
allow redundant cases in the list comprehension translation
2013-04-05, by traytel
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
2013-04-05, by traytel
tuned whitespace
2013-04-05, by traytel
Use Type.raw_match instead of Sign.typ_match
2013-04-04, by berghofe
special constant to prevent eta-contraction of the check-phase syntax of case translations
2013-04-05, by traytel
separate data used for case translation from the datatype package
2013-01-22, by traytel
case translations performed in a separate check phase (with adjustments by traytel)
2013-01-22, by berghofe
formal proof context for axclass proofs;
2013-04-10, by wenzelm
prefer local context;
2013-04-10, by wenzelm
proper proof context;
2013-04-10, by wenzelm
tuned;
2013-04-10, by wenzelm
merged
2013-04-09, by wenzelm
add command timings (like document command status);
2013-04-09, by wenzelm
tuned signature;
2013-04-09, by wenzelm
public Isabelle_Process.xml_cache (thread-safe);
2013-04-09, by wenzelm
tuned signature;
2013-04-09, by wenzelm
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09, by wenzelm
clarified protocol_message undefinedness;
2013-04-09, by wenzelm
quote by Alan Kay;
2013-04-09, by wenzelm
more accurate documentation;
2013-04-09, by wenzelm
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09, by wenzelm
more accurate documentation of "(structure)" mixfix;
2013-04-09, by wenzelm
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
2013-04-09, by wenzelm
tuned comment;
2013-04-09, by wenzelm
just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-09, by wenzelm
tuned message;
2013-04-09, by wenzelm
handle case clashes on Mac file system by encoding goal numbers
2013-04-09, by blanchet
avoid duplicate "tcon_" names
2013-04-09, by blanchet
smoothly handle cyclic graphs
2013-04-09, by blanchet
compile + fixed naming convention
2013-04-09, by blanchet
reverted accidental changes to theory file + updated wrt ML file
2013-04-09, by blanchet
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
2013-04-09, by blanchet
work on CASC LTB ISA exporter
2013-04-09, by blanchet
tuning
2013-04-09, by blanchet
add continuous_on rules for products
2013-04-09, by hoelzl
fixed spelling
2013-04-09, by hoelzl
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09, by hoelzl
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-04-09, by hoelzl
improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08, by wenzelm
prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-04-08, by wenzelm
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
2013-04-08, by wenzelm
discontinued odd magic number, which was once used for performance measurements;
2013-04-08, by wenzelm
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
2013-04-08, by wenzelm
merged
2013-04-08, by wenzelm
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
2013-04-08, by wenzelm
try to preserve original linearization
2013-04-08, by blanchet
use somewhat lighter encoding
2013-04-08, by blanchet
robustness w.r.t. unknown arguments
2013-04-08, by blanchet
cleaned
2013-04-07, by nipkow
cleaned
2013-04-07, by nipkow
tuned
2013-04-06, by nipkow
tuned signature -- agree with markup terminology;
2013-04-05, by wenzelm
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-05, by wenzelm
tuned document
2013-04-05, by nipkow
tuned
2013-04-05, by nipkow
sup on multisets
2013-04-04, by haftmann
convenient induction rule
2013-04-04, by haftmann
tuned README -- less buzzwords;
2013-04-04, by wenzelm
more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);
2013-04-04, by wenzelm
added missing file;
2013-04-04, by wenzelm
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by wenzelm
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04, by wenzelm
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04, by wenzelm
tuned imports;
2013-04-04, by wenzelm
added var_position in analogy to longid_position, for typing reports on input;
2013-04-04, by wenzelm
removed unnerving (esp in jedit) and pointless warning
2013-04-04, by nipkow
tuned
2013-04-04, by nipkow
merged
2013-04-03, by wenzelm
tuned;
2013-04-03, by wenzelm
recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03, by wenzelm
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-04-03, by wenzelm
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-03, by wenzelm
updated comment to 46b90bbc370d;
2013-04-03, by wenzelm
recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
2013-04-03, by wenzelm
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
2013-04-03, by wenzelm
tuned output -- less bullets;
2013-04-03, by wenzelm
default implementation of multisets by list with reasonable coverage of operations on multisets
2013-04-03, by haftmann
optionalized very specific code setup for multisets
2013-04-03, by haftmann
generalized lemma fold_image thanks to Peter Lammich
2013-04-03, by haftmann
tuned;
2013-04-02, by wenzelm
NEWS for 635562bc14ef;
2013-04-02, by wenzelm
more centralized command timing;
2013-04-02, by wenzelm
got rid of legacy smartness
2013-04-02, by blanchet
added lemma
2013-04-01, by nipkow
merged
2013-03-30, by wenzelm
amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
2013-03-30, by wenzelm
more formal cong_name;
2013-03-30, by wenzelm
timing status for forked diagnostic commands;
2013-03-30, by wenzelm
tooltip of command keyword includes timing information;
2013-03-30, by wenzelm
more operations on Time, Timing;
2013-03-30, by wenzelm
reverted slip introduced in f738e6dbd844
2013-03-29, by haftmann
added 'print_defn_rules' command;
2013-03-30, by wenzelm
more item markup;
2013-03-30, by wenzelm
item markup for Proof_Context.pretty_fact;
2013-03-30, by wenzelm
obsolete, cf. Proof_Context.print_syntax;
2013-03-30, by wenzelm
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
2013-03-29, by wenzelm
Pretty.item markup for improved readability of lists of items;
2013-03-29, by wenzelm
tuned message;
2013-03-29, by wenzelm
convenience check for vain instantiation
2013-03-29, by haftmann
improved centering via strikethrough offset;
2013-03-29, by wenzelm
re-generated SMT certificates
2013-03-28, by boehmes
new, simpler implementation of monomorphization;
2013-03-28, by boehmes
ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-28, by wenzelm
replace induction by hammer
2013-03-28, by kleing
merged
2013-03-28, by wenzelm
merged;
2013-03-28, by wenzelm
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
2013-03-28, by wenzelm
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
2013-03-28, by wenzelm
tuned;
2013-03-28, by wenzelm
proper default browser info for interactive mode, notably thy_deps;
2013-03-28, by wenzelm
improved pretty printing for state set acom
2013-03-28, by nipkow
Improvements to the print_dependencies command.
2013-03-27, by ballarin
discontinued obsolete parallel_proofs_reuse_timing;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
2013-03-27, by wenzelm
merged
2013-03-27, by wenzelm
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
2013-03-27, by wenzelm
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-03-27, by wenzelm
more liberal handling of skipped proofs;
2013-03-27, by wenzelm
explicit Toplevel.is_skipped_proof;
2013-03-27, by wenzelm
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27, by wenzelm
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-27, by wenzelm
clarified Skip_Proof.cheat_tac: more standard tactic;
2013-03-27, by wenzelm
tuned signature and module arrangement;
2013-03-27, by wenzelm
tuned;
2013-03-27, by wenzelm
tuned GUI;
2013-03-27, by wenzelm
centralized various multiset operations in theory multiset;
2013-03-27, by haftmann
avoid odd foundational terms after interpretation;
2013-03-26, by haftmann
more uniform style for interpretation and sublocale declarations
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
tuned session specification;
2013-03-26, by wenzelm
tuned proof;
2013-03-26, by wenzelm
tuned imports;
2013-03-26, by wenzelm
tuned proofs;
2013-03-26, by wenzelm
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
proper input event handling;
2013-03-26, by wenzelm
more standard imports;
2013-03-26, by wenzelm
more specific Entry painting;
2013-03-26, by wenzelm
tuned;
2013-03-26, by wenzelm
mixed theory/command entries;
2013-03-26, by wenzelm
dockable window for timing information;
2013-03-26, by wenzelm
no \FIXME macro for ProgProve (moved to book)
2013-03-26, by kleing
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26, by hoelzl
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26, by hoelzl
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26, by hoelzl
Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26, by hoelzl
move Ln.thy and Log.thy to Transcendental.thy
2013-03-26, by hoelzl
move SEQ.thy and Lim.thy to Limits.thy
2013-03-26, by hoelzl
HOL-NSA should only import Complex_Main
2013-03-26, by hoelzl
rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26, by hoelzl
rename RealDef to Real
2013-03-26, by hoelzl
remove Real.thy
2013-03-26, by hoelzl
merge RComplete into RealDef
2013-03-26, by hoelzl
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26, by hoelzl
remove posreal_complete
2013-03-26, by hoelzl
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-26, by hoelzl
Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25, by ballarin
Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25, by ballarin
Fix issue related to mixins in roundup.
2013-03-25, by ballarin
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
2013-03-25, by kleing
added lemmas
2013-03-25, by nipkow
merged
2013-03-25, by wenzelm
clarified text_fold vs. fbrk;
2013-03-25, by wenzelm
tuned print_classes: more standard order, markup, formatting;
2013-03-25, by wenzelm
tuned message;
2013-03-25, by wenzelm
actually exit on scalac failure;
2013-03-25, by wenzelm
tuned signature;
2013-03-25, by wenzelm
removed obsolete uses of ext
2013-03-25, by kleing
prefer preset = 3 -- much faster and less memory requirement;
2013-03-24, by wenzelm
basic support for xz files;
2013-03-24, by wenzelm
added component xz-java-1.2;
2013-03-24, by wenzelm
more "quick start" hints;
2013-03-24, by wenzelm
simple case syntax for stream (stolen from AFP/Coinductive)
2013-03-24, by traytel
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
2013-03-23, by wenzelm
merged
2013-03-23, by wenzelm
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
2013-03-23, by wenzelm
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
2013-03-23, by wenzelm
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23, by wenzelm
apply small result immediately, to avoid visible delay of text update after window move;
2013-03-23, by wenzelm
structural equality for Command.Results;
2013-03-23, by wenzelm
allow fractional pretty margin -- avoid premature rounding;
2013-03-23, by wenzelm
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
2013-03-23, by wenzelm
tuned;
2013-03-23, by wenzelm
spelling
2013-03-23, by haftmann
fundamental revision of big operators on sets
2013-03-23, by haftmann
tuned proof
2013-03-23, by haftmann
locales for abstract orders
2013-03-23, by haftmann
merged
2013-03-23, by krauss
added rudimentary induction rule for partial_function (heap)
2013-03-22, by krauss
allow induction predicates with arbitrary arity (not just binary)
2013-03-22, by krauss
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
2013-03-22, by hoelzl
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
2013-03-22, by hoelzl
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22, by hoelzl
move connected to HOL image; used to show intermediate value theorem
2013-03-22, by hoelzl
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
2013-03-22, by hoelzl
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-22, by hoelzl
clean up lemma_nest_unique and renamed to nested_sequence_unique
2013-03-22, by hoelzl
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
2013-03-22, by hoelzl
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-22, by hoelzl
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
2013-03-22, by hoelzl
move first_countable_topology to the HOL image
2013-03-22, by hoelzl
move metric_space to its own theory
2013-03-22, by hoelzl
move topological_space to its own theory
2013-03-22, by hoelzl
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
2013-03-21, by wenzelm
eliminated char_width_int to avoid unclear rounding;
2013-03-21, by wenzelm
proofs depend only on constraints, not on def of L WHILE
2013-03-21, by nipkow
use the right role for SPASS hypotheses
2013-03-20, by blanchet
soundness statement as in type system
2013-03-20, by kleing
add label for referencing in semantics book
2013-03-20, by kleing
tuned
2013-03-20, by nipkow
get rid of xcolor warnings
2013-03-19, by nipkow
extended stream library
2013-03-19, by traytel
export datatype definition which gets expanded too much in antiquotation
2013-03-19, by kleing
tuned
2013-03-19, by nipkow
add induction rule for partial_function (tailrec)
2013-03-19, by Andreas Lochbihler
prefer ownerless window, to avoid question of potentially changing parent view;
2013-03-18, by wenzelm
proper parent component for window.init;
2013-03-18, by wenzelm
lemma names and a corollary
2013-03-18, by kleing
managed to eliminate further snippets
2013-03-18, by kleing
fewer IMP snippets
2013-03-18, by kleing
merged
2013-03-18, by wenzelm
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
2013-03-18, by wenzelm
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
2013-03-18, by wenzelm
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
2013-03-17, by wenzelm
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
2013-03-17, by wenzelm
tuned
2013-03-18, by nipkow
eliminate duplicated constant (diag vs. Id_on)
2013-03-18, by traytel
hide internal constants; tuned proofs
2013-03-18, by traytel
tuned
2013-03-18, by nipkow
tuned
2013-03-17, by nipkow
added advanced rule induction subsection
2013-03-17, by nipkow
merged
2013-03-16, by wenzelm
more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
2013-03-16, by wenzelm
some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
2013-03-16, by wenzelm
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
2013-03-16, by wenzelm
drop a workaround because of 8739f8abbecb
2013-03-16, by kuncar
fixing transfer tactic - unfold fully identity relation by using relator_eq
2013-03-16, by kuncar
tuned (in particular bold fonts)
2013-03-16, by nipkow
merged
2013-03-16, by wenzelm
document ISABELLE_POLYML;
2013-03-14, by wenzelm
tuned
2013-03-15, by nipkow
simplified time_CPU and time_GC;
2013-03-15, by wenzelm
updated to scala-2.10.1;
2013-03-15, by wenzelm
extended stream library (sdrop_while)
2013-03-15, by traytel
tuned signature;
2013-03-14, by wenzelm
more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;
2013-03-14, by wenzelm
proper use of "member", without embarking on delicate questions about SML equality types;
2013-03-14, by wenzelm
made SML/NJ happy;
2013-03-14, by wenzelm
tuned
2013-03-14, by nipkow
merged
2013-03-13, by wenzelm
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
2013-03-13, by wenzelm
proper formatting, to facilitate line-based diff;
2013-03-13, by wenzelm
more uniform session descriptions, which show up in chapter index;
2013-03-13, by wenzelm
proper index for HOL-Proofs, which is also in chapter "HOL";
2013-03-13, by wenzelm
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
2013-03-13, by wenzelm
more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;
2013-03-13, by wenzelm
sessions may be organized via 'chapter' in ROOT;
2013-03-13, by wenzelm
do not absorb I/O errors;
2013-03-13, by wenzelm
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
2013-03-13, by wenzelm
new lemma subset_decode_imp_le
2013-03-13, by paulson
merged
2013-03-13, by kleing
more IMP snippets
2013-03-13, by kleing
rename fset_member to fmember and prove parametricity
2013-03-13, by kuncar
BNF uses fset defined via Lifting/Transfer rather than Quotient
2013-03-13, by traytel
nitpick setup and code generation for streams
2013-03-13, by traytel
merged
2013-03-13, by nipkow
tuned
2013-03-13, by nipkow
proper path -- I/O was hidden due to permissiveness;
2013-03-12, by wenzelm
merged
2013-03-12, by wenzelm
removed odd cvs artifacts;
2013-03-12, by wenzelm
refurbished some old README.html files as session descriptions, which show up in chapter index;
2013-03-12, by wenzelm
include session description in chapter index;
2013-03-12, by wenzelm
tuned;
2013-03-12, by wenzelm
more accurate theory links;
2013-03-12, by wenzelm
discontinued "isabelle usedir" option -r (reset session path);
2013-03-12, by wenzelm
discontinued "isabelle usedir" option -P (remote path);
2013-03-11, by wenzelm
support for 'chapter' specifications within session ROOT;
2013-03-11, by wenzelm
added latex markup
2013-03-12, by nipkow
merged
2013-03-12, by kleing
more snippets
2013-03-12, by kleing
added pairs
2013-03-12, by nipkow
extended set comprehension notation with {pttrn : A . P}
2013-03-12, by nipkow
tuned
2013-03-11, by nipkow
more factorisation of Step & Co
2013-03-11, by nipkow
factored out Step
2013-03-10, by nipkow
merged
2013-03-10, by nipkow
stepwise instantiation is more modular
2013-03-10, by nipkow
generalized subclass relation;
2013-03-10, by haftmann
termination proof for narrowing: fewer assumptions
2013-03-10, by nipkow
accomodate encrypted file-system on linux;
2013-03-09, by wenzelm
tuned;
2013-03-09, by wenzelm
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
2013-03-09, by haftmann
updated keywords (cf. 84d01fd733cf);
2013-03-08, by wenzelm
proper type inference for default values
2013-03-08, by blanchet
convert mappings to parametric lifting
2013-03-08, by kuncar
setup_lifting doesn't support a type variable as a raw type
2013-03-08, by kuncar
add [relator_mono] and [relator_distr] rules
2013-03-08, by kuncar
simplify Lift_FSet because we have parametricity in Lifting now
2013-03-08, by kuncar
patch Isabelle ditribution to conform to changes regarding the parametricity
2013-03-08, by kuncar
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
2013-03-08, by kuncar
merged
2013-03-08, by nipkow
simplified basic termination proof
2013-03-08, by nipkow
some simp rules for fset
2013-03-08, by traytel
avoid -Infinity which confuses JFreeChart histogram;
2013-03-07, by wenzelm
tuned proofs -- more structure, less warnings;
2013-03-07, by wenzelm
tuned signature -- prefer terminology of Scala and Axiom;
2013-03-07, by wenzelm
better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
2013-03-07, by blanchet
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
2013-03-06, by huffman
netlimit is abbreviation for Lim
2013-03-06, by hoelzl
tuned proofs
2013-03-06, by hoelzl
changed has_derivative_intros into a named theorems collection
2013-03-06, by hoelzl
changed continuous_on_intros into a named theorems collection
2013-03-06, by hoelzl
changed continuous_intros into a named theorems collection
2013-03-06, by hoelzl
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
2013-03-06, by hoelzl
major redesign: order instead of preorder, new definition of intervals as quotients
2013-03-06, by nipkow
added lemma
2013-03-06, by nipkow
extended numerals
2013-03-06, by nipkow
merged
2013-03-05, by wenzelm
merged
2013-03-05, by wenzelm
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-05, by wenzelm
extended stream library a little more
2013-03-05, by traytel
extended stream library
2013-03-05, by traytel
generalized lemmas in Extended_Real_Limits
2013-03-05, by hoelzl
eventually nhds represented using sequentially
2013-03-05, by hoelzl
generalized compact_Times to topological_space
2013-03-05, by hoelzl
move lemma Inf to usage point
2013-03-05, by hoelzl
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
2013-03-05, by hoelzl
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
2013-03-05, by hoelzl
generalized continuous/compact_attains_inf/sup from real to linorder_topology
2013-03-05, by hoelzl
continuity of pair operations
2013-03-05, by hoelzl
use generate_topology for second countable topologies, does not require intersection stable basis
2013-03-05, by hoelzl
generalized isGlb_unique
2013-03-05, by hoelzl
complete_linorder is also a complete_distrib_lattice
2013-03-05, by hoelzl
move Liminf / Limsup lemmas on complete_lattices to its own file
2013-03-05, by hoelzl
merged
2013-03-05, by nipkow
New theory of infinity-extended types; should replace Extended_xyz eventually
2013-03-05, by nipkow
Avoid ML warning about unreferenced identifier.
2013-03-05, by webertj
polymorphic SPASS is also SPASS
2013-03-05, by blanchet
allow more general coercion maps; tuned;
2013-03-05, by traytel
more lemmas about intervals
2013-03-05, by nipkow
merged
2013-03-04, by wenzelm
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-03-04, by wenzelm
join all proofs before scheduling present phase (ordered according to weight);
2013-03-04, by wenzelm
more explicit datatype result;
2013-03-04, by wenzelm
split dense into inner_dense_order and no_top/no_bot
2013-02-20, by hoelzl
move auxiliary lemmas from Library/Extended_Reals to HOL image
2013-02-20, by hoelzl
tuned (extend datatype to inline option)
2013-03-04, by traytel
prefer more systematic Future.flat;
2013-03-03, by wenzelm
more uniform Future.map: always internalize failure;
2013-03-03, by wenzelm
uniform treatment of global/local proofs;
2013-03-03, by wenzelm
tuned;
2013-03-03, by wenzelm
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-03-03, by wenzelm
more Thy_Syntax.element operations;
2013-03-03, by wenzelm
coercion-invariant arguments at work
2013-03-01, by traytel
constants with coercion-invariant arguments (possibility to disable/reenable
2013-03-01, by traytel
simplified Proof.future_proof;
2013-02-28, by wenzelm
provide explicit dummy names (cf. dfe469293eb4);
2013-02-28, by wenzelm
discontinued empty name bindings in 'axiomatization';
2013-02-28, by wenzelm
provide common HOLogic.conj_conv and HOLogic.eq_conv;
2013-02-28, by wenzelm
just one HOLogic.Trueprop_conv, with regular exception CTERM;
2013-02-28, by wenzelm
discontinued obsolete 'axioms' command;
2013-02-28, by wenzelm
more robust build error handling, e.g. missing outer syntax commands;
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm