isabelle: Graph

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
eliminated legacy 'axioms';
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm
eliminated legacy 'axioms';
2013-02-28, by wenzelm
marginalized historic strip_tac;
2013-02-28, by wenzelm
tuned proof;
2013-02-28, by wenzelm
tuned whitespace and indentation;
2013-02-28, by wenzelm
simplified imports;
2013-02-28, by wenzelm
load timings in parallel for improved performance;
2013-02-28, by wenzelm
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
2013-02-28, by wenzelm
parallel dep.load_files saves approx. 1s on 4 cores;
2013-02-27, by wenzelm
eliminated pointless re-ified errors;
2013-02-27, by wenzelm
merged
2013-02-27, by wenzelm
discontinued redundant 'use' command;
2013-02-27, by wenzelm
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27, by wenzelm
discontinued obsolete 'uses' within theory header;
2013-02-27, by wenzelm
use lemma from Big_Operators
2013-02-27, by Andreas Lochbihler
add inclusion/exclusion lemma
2013-02-27, by Andreas Lochbihler
added lemma
2013-02-27, by Andreas Lochbihler
merged
2013-02-27, by Andreas Lochbihler
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
2013-02-27, by Andreas Lochbihler
updated Toplevel.command_exception;
2013-02-26, by wenzelm
tuned;
2013-02-26, by wenzelm
tuned signature;
2013-02-26, by wenzelm
fork diagnostic commands (theory loader and PIDE interaction);
2013-02-26, by wenzelm
disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;
2013-02-26, by wenzelm
tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;
2013-02-26, by wenzelm
signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;
2013-02-26, by wenzelm
less eventful shutdown: merely wait for scheduler to terminate;
2013-02-26, by wenzelm
tuned messages;
2013-02-26, by wenzelm
tuned;
2013-02-26, by wenzelm
merged;
2013-02-25, by wenzelm
more explicit Goal.shutdown_futures;
2013-02-25, by wenzelm
reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
2013-02-25, by wenzelm
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
2013-02-25, by wenzelm
clarified Toplevel.element_result: scheduling policies happen here;
2013-02-25, by wenzelm
prefer stateless 'ML_val' for tests;
2013-02-25, by wenzelm
tuned comment;
2013-02-25, by wenzelm
reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
2013-02-25, by wenzelm
merged;
2013-02-25, by wenzelm
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
2013-02-24, by wenzelm
tuned;
2013-02-24, by wenzelm
unified Command.is_proper in ML with Scala (see also 123be08eed88);
2013-02-24, by wenzelm
tuned order of modules;
2013-02-25, by wenzelm
fixed document;
2013-02-25, by wenzelm
turned example into library for comparing growth of functions
2013-02-24, by haftmann
corrected reference
2013-02-24, by haftmann
improved orderings
2013-02-24, by nipkow
tuned agressiveness of isar compression
2013-02-24, by smolkas
eliminated isize in favour of size + type coercion
2013-02-24, by kleing
make SML/NJ happy;
2013-02-23, by wenzelm
basic setup for appbundler-1.0 for Mac OS X and Java 7;
2013-02-23, by wenzelm
more robust handling of repeated interrupts while terminating managed process;
2013-02-23, by wenzelm
more friendly message for spurious InterruptedException, which might still occur due to JVM oddities;
2013-02-23, by wenzelm
more explicit GUI components for dynamic actions;
2013-02-23, by wenzelm
clarified Progress.stopped: rising edge only;
2013-02-23, by wenzelm
more explicit console interrupt handling;
2013-02-23, by wenzelm
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
2013-02-23, by wenzelm
support for POSIX interrupts (bypassed on Windows);
2013-02-23, by wenzelm
merged
2013-02-22, by traytel
tuned error messages
2013-02-22, by traytel
Coercion_Examples defines required coercions itself (no Complex_Main needed)
2013-02-22, by traytel
apply unifying substitution before building the constraint graph
2013-02-22, by traytel
more abstract intervals
2013-02-22, by nipkow
more robust load_timings: ignore XML.Decode errors as well;
2013-02-22, by wenzelm
make SML/NJ happy;
2013-02-22, by wenzelm
identify exceptions more robustly, to allow SML/NJ report toplevel errors without crash;
2013-02-22, by wenzelm
make SML/NJ happy;
2013-02-22, by wenzelm
updated headers;
2013-02-22, by wenzelm
eliminated hard tabs;
2013-02-22, by wenzelm
discontinued obsolete src/HOL/IsaMakefile;
2013-02-22, by wenzelm
merged
2013-02-21, by wenzelm
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
2013-02-21, by wenzelm
merged
2013-02-21, by wenzelm
removed obsolete tags;
2013-02-21, by wenzelm
highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
2013-02-21, by wenzelm
tuned misleading message
2013-02-21, by blanchet
merged
2013-02-21, by wenzelm
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
2013-02-20, by wenzelm
prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;
2013-02-20, by wenzelm
more tight representation of command timing;
2013-02-20, by wenzelm
prefer comparison of session timing, if this is known already;
2013-02-20, by wenzelm
proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
2013-02-20, by wenzelm
support nested Thy_Syntax.element;
2013-02-20, by wenzelm
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
2013-02-19, by wenzelm
help JVM to cope with large symbolic structures;
2013-02-19, by wenzelm
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-02-19, by wenzelm
read logs from failed sessions as well;
2013-02-19, by wenzelm
recover timing information from old log files;
2013-02-19, by wenzelm
suppress timing message in full PIDE protocol -- this is for batch build;
2013-02-19, by wenzelm
support for build passing timings from Scala to ML;
2013-02-19, by wenzelm
support for prescient timing information within command transactions;
2013-02-19, by wenzelm
emit command_timing properties into build log;
2013-02-19, by wenzelm
generate Isar proof if Metis appears to be too slow
2013-02-21, by blanchet
swap slices so that the last slice is more complete (for minimization)
2013-02-21, by blanchet
tuning
2013-02-21, by blanchet
ensure all conjecture clauses are in the graph -- to prevent exceptions later
2013-02-20, by blanchet
generalize syntax of SPASS proofs
2013-02-20, by blanchet
tweaked hack some more
2013-02-20, by blanchet
more simplifying constructors
2013-02-20, by blanchet
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)
2013-02-20, by blanchet
more precise error
2013-02-20, by blanchet
improved hack
2013-02-20, by blanchet
upgraded to Alt-Ergo 0.95
2013-02-20, by blanchet
don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary
2013-02-20, by blanchet
trust preplayed proof in Mirabelle
2013-02-20, by blanchet
added case taken out by mistake
2013-02-20, by blanchet
tuning (removed redundant datatype)
2013-02-20, by blanchet
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
2013-02-20, by blanchet
honor linearization option also in the evaluation driver
2013-02-20, by blanchet
got rid of rump support for Vampire definitions
2013-02-20, by blanchet
optimize Isar output some more
2013-02-20, by blanchet
turn off more evil Vampire options to facilitate Isar proof generation
2013-02-20, by blanchet
fixed typo in option name
2013-02-20, by blanchet
tuning
2013-02-20, by blanchet
use new skolemizer only if some skolems have two or more arguments -- otherwise the old skolemizer cannot get the arg order wrong
2013-02-20, by blanchet
slacker comparison for Skolems, to avoid trivial equations
2013-02-20, by blanchet
auto-minimizer should respect "isar_proofs = true"
2013-02-20, by blanchet
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
2013-02-20, by blanchet
alias for people like me
2013-02-20, by blanchet
dropped spurious left-over from 0a2371e7ced3
2013-02-19, by haftmann
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
2013-02-19, by blanchet
interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
2013-02-19, by blanchet
delete also predicates on relations when hiding an implementation of an abstract type
2013-02-19, by kuncar
reintroduced crucial sorting accidentally lost in 962190eab40d
2013-02-19, by blanchet
compile
2013-02-19, by blanchet
provide two modes for MaSh driver: linearized or real visibility
2013-02-19, by blanchet
implement (more) accurate computation of parents
2013-02-18, by blanchet
tuning
2013-02-18, by blanchet
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
2013-02-18, by smolkas
simplified byline, isar_qualifier
2013-02-18, by smolkas
tuned code: factored out parent computation
2013-02-18, by blanchet
tuned code
2013-02-18, by blanchet
simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)
2013-02-18, by Andreas Lochbihler
fundamentals about discrete logarithm and square root
2013-02-17, by haftmann
Sieve of Eratosthenes
2013-02-17, by haftmann
note on parallel computation
2013-02-17, by haftmann
corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
2013-02-17, by haftmann
simplified construction of upto_aux
2013-02-17, by haftmann
merged
2013-02-17, by haftmann
restored proper order of NEWS entries (lost due too long-waiting patches)
2013-02-16, by haftmann
CONTRIBUTORS
2013-02-17, by haftmann
tail recursive code for function "upto"
2013-02-16, by nipkow
tuning
2013-02-15, by blanchet
repaired collateral damage from 4f0147ed8bcb
2013-02-15, by blanchet
Backed out changeset: 3fe7242f8346,
2013-02-15, by traytel
dropped now obsolete hint;
2013-02-15, by haftmann
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
2013-02-15, by haftmann
systematic conversions between nat and nibble/char;
2013-02-15, by haftmann
coercions between base types can be lifted to sets
2013-02-15, by traytel
annotate obtains with types
2013-02-15, by blanchet
merge
2013-02-15, by blanchet
made check for conjecture skolemization sound
2013-02-15, by blanchet
use safe var index
2013-02-15, by smolkas
merged
2013-02-15, by Andreas Lochbihler
more type class instances for Numeral_Type (contributed by Jesus Aransay)
2013-02-15, by Andreas Lochbihler
added lemma
2013-02-15, by Andreas Lochbihler
merge
2013-02-15, by blanchet
merge
2013-02-15, by blanchet
skolemize conjecture properly in Isar proof
2013-02-15, by blanchet
tuning -- refactoring in preparation for handling skolemization of conjecture
2013-02-15, by blanchet
removed dead weight from data structure
2013-02-15, by blanchet
tuned code
2013-02-15, by blanchet
tuned code
2013-02-15, by blanchet
less customary term_of conversions;
2013-02-15, by haftmann
two target language numeral types: integer and natural, as replacement for code_numeral;
2013-02-15, by haftmann
explicit code equation for integer_of_nat
2013-02-15, by haftmann
extended stream library
2013-02-15, by traytel
merged
2013-02-15, by Andreas Lochbihler
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
2013-02-15, by Andreas Lochbihler
killed legacy alias
2013-02-15, by blanchet
updated news
2013-02-15, by blanchet
avoid crude/wrong theorem comparision
2013-02-15, by blanchet
tuned code
2013-02-15, by blanchet
more MaSh tracing
2013-02-15, by blanchet
tuning
2013-02-15, by blanchet
fixed metis_steps_total - was off by one
2013-02-14, by smolkas
preplay subblocks
2013-02-14, by smolkas
renamed sledgehammer_shrink to sledgehammer_compress
2013-02-14, by smolkas
dont skolemize conjecture
2013-02-14, by smolkas
introduced subblock in isar_step datatype for conjecture herbrandization
2013-02-14, by smolkas
write_pdf for JFreeChart;
2013-02-14, by wenzelm
reform of predicate compiler / quickcheck theories:
2013-02-14, by haftmann
merged
2013-02-14, by Andreas Lochbihler
instantiate finite_UNIV and card_UNIV for finfun type
2013-02-14, by Andreas Lochbihler
merged
2013-02-14, by wenzelm
more parallel proofs in 'nominal_datatype', although sequential dark matter remains;
2013-02-14, by wenzelm
tuned proof;
2013-02-14, by wenzelm
obsolete;
2013-02-14, by wenzelm
tuned proofs;
2013-02-14, by wenzelm
tuned signature -- legacy packages might want to fork proofs as well;
2013-02-14, by wenzelm
merged
2013-02-14, by Andreas Lochbihler
implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
2013-02-14, by Andreas Lochbihler
consolidation of library theories on product orders
2013-02-14, by haftmann
type lifting setup for code numeral types
2013-02-14, by haftmann
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
2013-02-14, by haftmann
abandoned theory Plain
2013-02-14, by haftmann
tuned;
2013-02-14, by wenzelm
clarified default according to etc/options;
2013-02-13, by wenzelm
Java assumes regular "re-parenting" window manager;
2013-02-13, by wenzelm
merged
2013-02-13, by immler
complete metric for formal power series
2013-02-13, by immler
eliminated union_closed_basis; cleanup Fin_Map
2013-02-13, by immler
fine grained instantiations
2013-02-13, by immler
use maximum norm for type finmap
2013-02-13, by immler
generalized
2013-02-13, by immler
generalized
2013-02-13, by immler
merged
2013-02-13, by wenzelm
discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;
2013-02-13, by wenzelm
more thorough error handling of load/save (see also c1be3072ea8f);
2013-02-13, by wenzelm
file system operations for Graphics2D output;
2013-02-13, by wenzelm
updated isabelle-release URLs;
2013-02-13, by wenzelm
combinator List.those;
2013-02-13, by haftmann
explicit conversion integer_of_nat already in Code_Numeral_Types;
2013-02-13, by haftmann
IArray ignorant of particular representation of nat
2013-02-13, by haftmann
tuned, particulary name
2013-02-13, by haftmann
formal cleanup of sources
2013-02-13, by haftmann
another attempt for a uniform abort on code generation errors
2013-02-13, by haftmann
tuned spelling
2013-02-13, by haftmann
removed obsolete RC tags;
2013-02-13, by wenzelm
merged;
2013-02-13, by wenzelm
detect more hosts;
2013-02-12, by wenzelm
Added tag Isabelle2013 for changeset d90218288d51
2013-02-12, by wenzelm
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski; Isabelle2013
2013-02-11, by wenzelm
merged
2013-02-10, by wenzelm
avoid crash (NPE) when properties are changed during prover startup (e.g. by font scaling);
2013-02-10, by wenzelm
updated PIDE notes;
2013-02-10, by wenzelm
proper root for document variants (cf. be8002ee43d8);
2013-02-07, by wenzelm
Added tag Isabelle2013-RC3 for changeset 8cf38c6b33f8
2013-02-07, by wenzelm
proforma update to jdk-7u13 -- barely relevant security updates by Oracle;
2013-02-06, by wenzelm
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
2013-02-06, by wenzelm
documentation for 'print_rules';
2013-02-06, by wenzelm
no choice of target directory -- default file permissions outside user directory tend to be ill-defined for Cygwin;
2013-02-01, by wenzelm
merged
2013-02-01, by wenzelm
provide jdk-7u13 (still inactive, potentially pointless);
2013-02-01, by wenzelm
allow relative directory;
2013-02-01, by wenzelm
standardized isabelle-server.in.tum.de;
2013-02-01, by wenzelm
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
2013-01-31, by wenzelm
made SML/NJ happy
2013-01-28, by traytel
more portable alternative shortcuts on numeric keypad;
2013-01-28, by wenzelm
more generic reference to polyml component;
2013-01-28, by wenzelm
Added tag Isabelle2013-RC2 for changeset 7fc61bfb1c2d
2013-01-28, by wenzelm
updated to polyml-5.5.0-3 based on fixes-5.5 version 1658, which provides important improvements;
2013-01-28, by wenzelm
merged
2013-01-28, by wenzelm
separate makedist_bundle for each platform family, which is more useful for manual use;
2013-01-28, by wenzelm
tuned;
2013-01-28, by wenzelm
tuned;
2013-01-26, by wenzelm
notes on building Poly/ML;
2013-01-26, by wenzelm
tuned ML platform fallback;
2013-01-26, by wenzelm
manual update of sessions, based on "isabelle build -nvc";
2013-01-26, by wenzelm
some updates concerning Proof General;
2013-01-26, by wenzelm
updated explanations of document preparation;
2013-01-26, by wenzelm
clarified NEWS on isabelle build and mkroot;
2013-01-26, by wenzelm
some explanations of important build options;
2013-01-26, by wenzelm
tuned;
2013-01-26, by wenzelm
another attempt to standardize sort order in a portable way;
2013-01-25, by wenzelm
rebundled polyml-5.5.0-2, which now includes the sources as usual (e.q. required for formal references in Isabelle/ML);
2013-01-25, by wenzelm
updated for release;
2013-01-25, by wenzelm
tuned;
2013-01-25, by wenzelm
minimal updated of jEdit/README.html, without any substantial reforms;
2013-01-25, by wenzelm
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
2013-01-25, by wenzelm
avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;
2013-01-24, by wenzelm
report status more frequently on demand;
2013-01-24, by wenzelm
more efficient inlined properties, especially relevant for voluminous tasks trace;
2013-01-24, by wenzelm
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
2013-01-22, by wenzelm
repackaged polyml-5.5.0-1 -- only x86-cygwin changed;
2013-01-21, by wenzelm
better apply peflags at build time, to avoid antivirus getting nervous about changing executables;
2013-01-21, by wenzelm
Added tag Isabelle2013-RC1 for changeset 2c3d0cb151c0
2013-01-20, by wenzelm
tuned state display
2013-02-13, by nipkow
tuned names
2013-02-13, by nipkow
tuned
2013-02-12, by nipkow
tuned identifier
2013-02-12, by nipkow
tuned top
2013-02-12, by nipkow
Typo in description of abs_def.
2013-02-11, by webertj
distinguish one more kind of proofs
2013-02-08, by blanchet
added markers in proofs identifying origin of proofs, in eval driver
2013-02-08, by blanchet
added option to use SNoW as machine learning algo
2013-02-08, by blanchet
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
2013-02-07, by blanchet
more precise error message
2013-02-07, by blanchet
killed deadcode
2013-02-07, by blanchet
more robustness w.r.t. 0
2013-02-07, by blanchet
hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly
2013-02-07, by blanchet
tuned indent
2013-02-07, by blanchet
drop needless .0s
2013-02-07, by blanchet
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
2013-02-07, by blanchet
infix syntax for streams (reflecting the one for lists)
2013-02-07, by traytel
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
2013-02-06, by hoelzl
check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop
2013-02-06, by hoelzl
removed spurious trimming
2013-02-05, by blanchet
tuned
2013-02-04, by nipkow
tuned slicing (E-MaLeS and E-Par)
2013-02-03, by blanchet
tune slices further
2013-02-02, by blanchet
tweak ATP slices further
2013-02-02, by blanchet
compile
2013-01-31, by blanchet
also have SMT solvers alternate fact filter
2013-01-31, by blanchet
use the right filter in each slice
2013-01-31, by blanchet
tuned slices
2013-01-31, by blanchet
store fact filter along with ATP slice
2013-01-31, by blanchet
tuned data structure
2013-01-31, by blanchet
thread through fact triple component from which used facts come, for accurate index output
2013-01-31, by blanchet
more precise output of selected facts
2013-01-31, by blanchet
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
2013-01-31, by blanchet
simplified SMT solver code in Sledgehammer
2013-01-31, by blanchet
eliminated needless speed optimization -- and simplified code quite a bit
2013-01-31, by blanchet
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
2013-01-31, by blanchet
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
2013-01-31, by blanchet
remove unnecessary assumption from real_normed_vector
2013-01-31, by hoelzl
adapted to new MaSh interface
2013-01-31, by blanchet
use order topology for extended reals
2013-01-31, by hoelzl
introduce order topology
2013-01-31, by hoelzl
simplify heine_borel type class
2013-01-31, by hoelzl
compute proper weight for "p proves p" in MaSh
2013-01-31, by blanchet
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
2013-01-15, by kuncar
tuned
2013-01-25, by nipkow
back to post-release mode -- after fork point;
2013-01-20, by wenzelm
updated for release;
2013-01-20, by wenzelm
merged
2013-01-20, by wenzelm
misc tuning for release;
2013-01-20, by wenzelm
tuned;
2013-01-20, by wenzelm
accomodate scala-2.9.2;
2013-01-20, by wenzelm
afford parallel proof terms;
2013-01-19, by wenzelm
always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
2013-01-19, by wenzelm
simplified proofs
2013-01-19, by nipkow
tuning
2013-01-19, by blanchet
misc cleanup;
2013-01-19, by wenzelm
tuned signature;
2013-01-19, by wenzelm
use inlined session name as title for charts;
2013-01-18, by wenzelm
tuned signature;
2013-01-18, by wenzelm
charts for future task runtime statistics;
2013-01-18, by wenzelm
merged
2013-01-18, by wenzelm
more uniform permissions;
2013-01-18, by wenzelm
more generous C stack size as in Linux and Mac OS X, to reduce chance of Cygwin-specific crashes;
2013-01-18, by wenzelm
tuned proof -- much faster;
2013-01-18, by wenzelm
more systematic task statistics;
2013-01-18, by wenzelm
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-18, by wenzelm
generalized diameter from real_normed_vector to metric_space
2013-01-18, by hoelzl
tuned proof
2013-01-18, by hoelzl
tune prove compact_eq_totally_bounded
2013-01-18, by hoelzl
generalized theorem edelstein_fix to class metric_space
2013-01-17, by huffman
tuning
2013-01-18, by blanchet
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
2013-01-18, by blanchet
optimization -- evaluate conversion to table only once
2013-01-18, by blanchet
MeSh prover generation
2013-01-17, by blanchet
use correct weights in MeSh driver
2013-01-17, by blanchet
use precomputed MaSh/MePo data whenever available
2013-01-17, by blanchet
merged
2013-01-17, by wenzelm
merged
2013-01-17, by wenzelm
copy Cygwin-Latex-Setup.bat;
2013-01-17, by wenzelm
more formal Cygwin-Latex-Setup (excluding bulky texlive-collection-fontsextra, which would be required for eulervm.sty);
2013-01-17, by wenzelm
updated to cygwin-20130117;
2013-01-17, by wenzelm
proper permissions;
2013-01-17, by wenzelm
tuned;
2013-01-17, by wenzelm
updated to jdk-7u11;
2013-01-17, by wenzelm
simplify proof of compact_imp_bounded
2013-01-17, by huffman
added step to skip some queries
2013-01-17, by blanchet
provide a means to skip a method
2013-01-17, by blanchet
evaluate more cases (cf. paper)
2013-01-17, by blanchet
updated MaSh
2013-01-17, by blanchet
make SPASS more configurable, for experiments
2013-01-17, by blanchet
generalize more topology lemmas
2013-01-15, by huffman
generalize topology lemmas; simplify proofs
2013-01-15, by huffman
merged
2013-01-17, by wenzelm
tuned signature (again) -- keep Properties more generic;
2013-01-17, by wenzelm
tuned proofs;
2013-01-17, by wenzelm
simplified prove of compact_imp_bounded
2013-01-17, by hoelzl
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
2013-01-17, by hoelzl
move auxiliary lemma to top
2013-01-17, by hoelzl
add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
2013-01-17, by hoelzl
group compactness-eq-seq-compactness lemmas together
2013-01-17, by hoelzl
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
2013-01-17, by hoelzl
tuned
2013-01-17, by hoelzl
removed subseq_bigger (replaced by seq_suble)
2013-01-17, by hoelzl
countablility of finite subsets and rational numbers
2013-01-17, by hoelzl
generalize compact_path_image to topological_space
2013-01-17, by hoelzl
re-generated components.sha1;
2013-01-17, by wenzelm
merged
2013-01-17, by wenzelm
more system-independent order of components.sha1 to keep changes monotonic;
2013-01-17, by wenzelm
clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
2013-01-17, by wenzelm
delay to give users a chance to see what was happening, even with auto_close enabled;
2013-01-17, by wenzelm
updated docs
2013-01-17, by blanchet
updated component again, as there was an issue with hard-coded paths in "runepar.pl"
2013-01-17, by blanchet
added E-Par support
2013-01-17, by blanchet
updated E component
2013-01-17, by blanchet
tweaked defaults
2013-01-17, by blanchet
changed type of preplay time; tuned preplaying
2013-01-17, by smolkas
move preplaying to own structure
2013-01-17, by smolkas
register SHA1 for Haskabelle-2013 component
2013-01-17, by noschinl
register Haskabelle as a component
2013-01-17, by noschinl
merged
2013-01-16, by wenzelm
tuned proofs;
2013-01-16, by wenzelm
tuned proofs;
2013-01-16, by wenzelm
tuned signature;
2013-01-16, by wenzelm
proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
2013-01-16, by wenzelm
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
2013-01-16, by wenzelm
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16, by wenzelm
eliminated dead code;
2013-01-16, by wenzelm
proper range position;
2013-01-16, by wenzelm
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16, by wenzelm
tuned comments;
2013-01-16, by wenzelm
tuned signature;
2013-01-16, by wenzelm
use Pure instead of HOL connectives
2013-01-16, by smolkas
graceful failure
2013-01-16, by blanchet
honor fact range for MePo as well
2013-01-16, by blanchet
more improvements to Isar proof reconstructions
2013-01-15, by blanchet
tuned whitespace
2013-01-15, by blanchet
merged
2013-01-15, by wenzelm
avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
2013-01-15, by wenzelm
tuned;
2013-01-15, by wenzelm
separate color ranges by 1px to improve discernment of overall theory status;
2013-01-15, by wenzelm
grand-unified Admin/Release/build script (excluding .app and .exe);
2013-01-15, by wenzelm
generalized more topology theorems
2013-01-15, by huffman
generalize lemma islimpt_finite to class t1_space
2013-01-14, by huffman
tuned
2013-01-15, by nipkow
more prominent status ticks;
2013-01-14, by wenzelm
merged
2013-01-14, by wenzelm
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
2013-01-14, by wenzelm
include /isabelle/rebaseall in autorebaseall, which is run after installation of further packages;
2013-01-14, by wenzelm
do not register quasi-components, notably cygwin;
2013-01-14, by wenzelm
updated to jdk-7u11;
2013-01-14, by wenzelm
updated to cygwin-20130114;
2013-01-14, by wenzelm
clarified paths: init relatively to cygwin root;
2013-01-14, by wenzelm
avoid odd copies of local configuration or backup files;
2013-01-14, by wenzelm
more precise relevant_range to exploit overview_limit better;
2013-01-14, by wenzelm
restrict "bad" markup to command keyword, notably excluding subsequent comments;
2013-01-14, by wenzelm
differentiate (cover) compactness and sequential compactness
2013-01-14, by hoelzl
introduce first_countable_topology typeclass
2013-01-14, by hoelzl
move prod instantiation of second_countable_topology to its definition
2013-01-14, by hoelzl
renamed countable_basis_space to second_countable_topology
2013-01-14, by hoelzl
move eventually_Ball_finite to Limits
2013-01-14, by hoelzl
more update on Lifting in isar-ref
2013-01-14, by kuncar
NEWS
2013-01-14, by kuncar
update isar-ref for Quotient and Lifting package
2013-01-14, by kuncar
run Sledgehammer provers in parallel in "try"
2013-01-14, by blanchet
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
2013-01-14, by blanchet
adjust weights -- sorts are prolific, so tone them down even more
2013-01-14, by blanchet
merged
2013-01-13, by wenzelm
merged
2013-01-13, by wenzelm
more exhaustive full test, to avoid surprises with makedist_library;
2013-01-13, by wenzelm
hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
2013-01-13, by wenzelm
don't learn theories -- this option is very slow and not very helpful
2013-01-13, by blanchet
more informative output
2013-01-13, by blanchet
have Mirabelle produce more output
2013-01-13, by blanchet
tuned message
2013-01-13, by blanchet
merged
2013-01-13, by wenzelm
updated makedist_library;
2013-01-13, by wenzelm
some attempts to avoid "._" files on Mac OS X;
2013-01-13, by wenzelm
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
2013-01-13, by wenzelm
honor unknown chained in MaSh and a few other tweaks
2013-01-13, by blanchet
remove obsolete MaSh files
2013-01-13, by blanchet
don't generate queries with empty dependency list
2013-01-13, by blanchet
cleaned up hint handling
2013-01-13, by blanchet
better handlig of built-ins -- at the top-level, not in subterms
2013-01-13, by blanchet
tuned message;
2013-01-12, by wenzelm
proper window title;
2013-01-12, by wenzelm
add icon for toplevel windows;
2013-01-12, by wenzelm
lower bound to font size for the sake of Mac OS X (cf. 4cd2d090be8f);
2013-01-12, by wenzelm
forced scroll to bottom, for improved cross-platform appearance;
2013-01-12, by wenzelm
merged
2013-01-12, by wenzelm
tuned font size, notably for current HD displays;
2013-01-12, by wenzelm
more uniform Pretty.char_width;
2013-01-12, by wenzelm
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
2013-01-12, by wenzelm
tuned signature;
2013-01-12, by wenzelm
more uniform theory progress in build -v and build_dialog;
2013-01-12, by wenzelm
immediate theory progress for build_dialog;
2013-01-12, by wenzelm
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
2013-01-12, by wenzelm
removed unused/non-portable bash_output_fifo;
2013-01-12, by wenzelm
tuned signature;
2013-01-12, by wenzelm
honor filtering out of arguments for built-in constants (e.g. representation of numerals)
2013-01-12, by blanchet
new version of MaSh Python component
2013-01-12, by blanchet
prefer MS-DOS-style temp;
2013-01-11, by wenzelm
more Cygwin packages to help out in a pitch -- NB: make is still needed for legacy usedir;
2013-01-11, by wenzelm
merged
2013-01-11, by wenzelm
more NEWS;
2013-01-11, by wenzelm
proper path names;
2013-01-11, by wenzelm
refer to cygwin mirror with static copy of setup.ini;
2013-01-11, by wenzelm
discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
2013-01-11, by wenzelm
obsolete;
2013-01-11, by wenzelm
more standard contrib/cygwin location (again);
2013-01-11, by wenzelm
updated messages
2013-01-11, by blanchet
fixed escaping for MeSh encoder
2013-01-11, by blanchet
don't learn from the proof of "psimps" etc.
2013-01-11, by blanchet
updated MaSh Python component
2013-01-11, by blanchet
start using MaSh hints
2013-01-11, by blanchet
always compare theorem using the same, weaker function
2013-01-11, by blanchet
tuned
2013-01-11, by smolkas
set show_markup to false in order to avoid problems in jedit
2013-01-11, by smolkas
merged
2013-01-11, by nipkow
tuned
2013-01-11, by nipkow
merged
2013-01-11, by noschinl
added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)
2013-01-10, by noschinl
explicit references avoid dynamic lookup
2013-01-11, by haftmann
sharing of recursive results on evaluation
2013-01-11, by haftmann
removed debugging code
2013-01-10, by blanchet
make name table work the way it was intended to
2013-01-10, by blanchet
export MeSh data as well
2013-01-10, by blanchet
merged
2013-01-10, by wenzelm
manage cygwin as bundled quasi-component;
2013-01-10, by wenzelm
tuned;
2013-01-10, by wenzelm
outermost directory structure for Windows/Cygwin;
2013-01-10, by wenzelm
updated for release;
2013-01-10, by wenzelm
more general prover termination dialog, which might indicate undetected failure or just ML "exit 0";
2013-01-10, by wenzelm
clarified cygwin/isabelle scripts;
2013-01-10, by wenzelm
more systematic makedist_cygwin;
2013-01-10, by wenzelm
prefer system build mode in main application wrappers, to produce heaps insided distribution directory;
2013-01-10, by wenzelm
tuned proofs;
2013-01-10, by wenzelm
dock "Theories" right, although it might obscure some control buttons;
2013-01-10, by wenzelm
scala-2.9.2 is still supported;
2013-01-10, by wenzelm
made SML/NJ happy;
2013-01-10, by wenzelm
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
2013-01-10, by wenzelm
minor update;
2013-01-09, by wenzelm
purge other platforms uniformly;
2013-01-09, by wenzelm
unconditional jedit_build;
2013-01-09, by wenzelm
Console is not docked on startup;
2013-01-09, by wenzelm
refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;
2013-01-09, by wenzelm
renamed tool;
2013-01-09, by wenzelm
create required PREFS_DIR;
2013-01-09, by wenzelm
eliminated choosefrom -- power-users may edit global defaults within script;
2013-01-09, by wenzelm
tuned;
2013-01-09, by wenzelm
updated makebundles as Admin isabelle tool;
2013-01-09, by wenzelm
tuned;
2013-01-09, by wenzelm
Added proof function declarations for min and max
2013-01-10, by berghofe
disable interactive mode of Specification.theorem with its slow printing of results;
2013-01-08, by wenzelm
changed exception to uppercase
2013-01-09, by smolkas
proper exception handling; reraise interrupt exceptions
2013-01-09, by smolkas
more CHECKLIST;
2013-01-09, by wenzelm
merged
2013-01-09, by wenzelm
build browser more robustly before startup;
2013-01-09, by wenzelm
standardized treatment of timing properties;
2013-01-09, by wenzelm
consider merging obtain steps
2013-01-09, by smolkas
preplay obtain steps
2013-01-09, by smolkas
tune spelling;
2013-01-09, by wenzelm
include timing properties in log; build_history_base
2013-01-08, by wenzelm
merged
2013-01-08, by wenzelm
upper bound for font size;
2013-01-08, by wenzelm
more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";
2013-01-08, by wenzelm
more aggressive update -- potentially relevant for previously is_outdated output;
2013-01-08, by wenzelm
allow negative argument in "consumes" source format;
2013-01-08, by wenzelm
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
2013-01-08, by wenzelm
more direct invalidateScreenLineRange after changed assignment;
2013-01-08, by wenzelm
tuned;
2013-01-08, by wenzelm
tuned -- prefer high-level Table.merge with its slightly more conservative update;
2013-01-08, by wenzelm
tuned output
2013-01-08, by blanchet
tuned names
2013-01-08, by nipkow
merged;
2013-01-07, by wenzelm
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
2013-01-07, by wenzelm
no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;
2013-01-07, by wenzelm
merged
2013-01-07, by wenzelm
export some generally useful operations;
2013-01-06, by wenzelm
tuned comment -- do not claim anything;
2013-01-07, by wenzelm
cleaner context threading
2013-01-07, by blanchet
tuned output
2013-01-07, by blanchet
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
2013-01-07, by wenzelm
put single-theorem names before multi-theorem ones (broken since 5d147d492792)
2013-01-06, by blanchet
get rid of spurious "Isar" proofs
2013-01-06, by blanchet
also generate queries for goals with too many Isar dependencies
2013-01-06, by blanchet
updated to scala-2.10.0;
2013-01-06, by wenzelm
merged
2013-01-06, by blanchet
tuned message
2013-01-05, by blanchet
tap after, not before command invocation
2013-01-05, by blanchet
increased hard timeout -- minimization can take time
2013-01-05, by blanchet
nicer output
2013-01-05, by blanchet
pass option to minimize
2013-01-05, by blanchet
prefer apple.laf.useScreenMenuBar=true (despite cf. effcfa38e77b) to make it work better with full-screen mode;
2013-01-05, by wenzelm
ignore vacuous edits (e.g. stemming from Plugin.init_models) to avoid pointless protocol round-trip, which could lead to painting of outdated snapshot in the meantime (notably on Windows);
2013-01-05, by wenzelm
tuned JEDIT_JAVA_OPTIONS: increase chances that it works with approx. 8 cores and 32bit platform (notably Windows);
2013-01-05, by wenzelm
propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
2013-01-05, by wenzelm
premature window close means failure;
2013-01-05, by wenzelm
less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;
2013-01-05, by wenzelm
proper return code on window close;
2013-01-05, by wenzelm
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
2013-01-05, by wenzelm
more direct property names;
2013-01-05, by wenzelm
tuned -- less indirection;
2013-01-05, by wenzelm
tuned blacklisting in relevance filter
2013-01-05, by blanchet
refined class handling, to prevent cycles in fact graph
2013-01-04, by blanchet
learn from low-level, inside-class facts
2013-01-04, by blanchet
tuning
2013-01-04, by blanchet
tweaked nicknames
2013-01-04, by blanchet
merged
2013-01-04, by wenzelm
more reactive completion popup by default;
2013-01-04, by wenzelm
actually install required copy of Highlight.jar;
2013-01-04, by wenzelm
updated to jedit_build-20130104;
2013-01-04, by wenzelm
another attempt to get Mac OS X keyhandling right: ALTERNATIVE_DISPATCHER is off, but ALT_KEY_PRESSED_DISABLED is more careful to interpret ALT like ALT_GRAPH, which does not count as modifier here (NB: CONTROL + ALT means ALT_GRAPH on Windows, but ALT means ALT_GRAPH on Mac OS X);
2013-01-04, by wenzelm
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
2013-01-04, by wenzelm
tuned imports;
2013-01-04, by wenzelm
support TAB in completion: need to configure the component with the key handler;
2013-01-04, by wenzelm
note to eliminate dynamic name reference
2013-01-04, by haftmann
speed up generation of local theorem nicknames
2013-01-04, by blanchet
speed up nickname generation for local facts
2013-01-04, by blanchet
updated docs
2013-01-04, by blanchet
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
2013-01-04, by blanchet
tweaked fudge factor
2013-01-04, by blanchet
more NEWS;
2013-01-04, by wenzelm
document 'locale_deps';
2013-01-04, by wenzelm
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
2013-01-04, by wenzelm
more formal inlining of system information;
2013-01-04, by wenzelm
tuned message -- suppress inlined system information;
2013-01-04, by wenzelm
merged
2013-01-04, by smolkas
tuned
2013-01-03, by smolkas
avoid long enumeration of HO unifiers;
2013-01-03, by wenzelm
disable search dialog pool on all platforms -- to prevent GUI synchronization problems seen on KDE (e.g. Kubuntu 12.10);
2013-01-03, by wenzelm
merged
2013-01-03, by wenzelm
maintain session index on Scala side, for more determistic results;
2013-01-03, by wenzelm
close formulas in the natural order, not its reverse -- so that Skolem arguments appear in the right order in Isar proofs
2013-01-03, by blanchet
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2013-01-03, by blanchet
rename variable in binder, not just in body
2013-01-03, by blanchet
swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases)
2013-01-03, by blanchet
tuned comment
2013-01-03, by blanchet
NEWS: ML runtime statistics;
2013-01-03, by wenzelm
merged
2013-01-03, by wenzelm
more interesting fields;
2013-01-03, by wenzelm
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
2013-01-03, by wenzelm
improved Monitor_Dockable, based on ML_Statistics operations;
2013-01-03, by wenzelm
get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification
2013-01-03, by blanchet
avoid explosion in higher-order unification algorithm
2013-01-03, by blanchet
avoid repeated calls to metis from "resolve_tac" in case of ultimate failure
2013-01-03, by blanchet
tuned comment
2013-01-03, by blanchet
merged
2013-01-02, by wenzelm
added standard_frames convenience;
2013-01-02, by wenzelm
some grouping of standard fields;
2013-01-02, by wenzelm
some support for chart drawing;
2013-01-02, by wenzelm
some support for ML statistics content interpretation;
2013-01-02, by wenzelm
moved files;
2013-01-02, by wenzelm
moved files;
2013-01-02, by wenzelm
ML runtime statistics: read properties from build log;
2013-01-02, by wenzelm
support File.read_gzip as well, in accordance to File.write_gzip;
2013-01-02, by wenzelm
inline ML statistics into build log;
2013-01-02, by wenzelm
removed outdated comment;
2013-01-02, by wenzelm
enable Z3 for full test (cf. 6f48853f08d5);
2013-01-02, by wenzelm
removed old, unused code
2013-01-02, by smolkas
removed whitespace
2013-01-02, by smolkas
removed duplicate code
2013-01-02, by smolkas
use rpair to avoid swap
2013-01-02, by smolkas
generate "obtain" steps corresponding to skolemization inferences
2013-01-02, by blanchet
keep E's and Vampire's skolemization steps
2013-01-02, by blanchet
tuning
2013-01-02, by blanchet
fixed oversensitive Skolem handling (cf. eaa540986291)
2013-01-02, by blanchet
added "obtain" to Isar proof construction data structure
2013-01-02, by blanchet
tuning
2013-01-02, by blanchet
properly take the existential closure of skolems
2013-01-02, by blanchet
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
2013-01-02, by blanchet
tuning
2013-01-02, by blanchet
added 112 to list of known Z3 error codes
2013-01-02, by blanchet
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
2013-01-02, by blanchet
added missing certificate file to "ROOT"
2013-01-02, by blanchet
more robust report_status: tolerate ML_statistics even if ignored right now, e.g. in batch build;
2013-01-01, by wenzelm
more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
2013-01-01, by wenzelm
regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
2013-01-01, by blanchet
Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently
2013-01-01, by blanchet
dropped relics of ancient side-entry points
2013-01-01, by haftmann
prefer JDialog over JWindow to avoid focus inversion problem on Compiz (e.g. Ubuntu/Unity 12.10): both JDialog and JFrame happen to work, but JFrame does not support parent nesting;
2012-12-31, by wenzelm
tuned signature;
2012-12-31, by wenzelm
tuned imports;
2012-12-31, by wenzelm
include user counters as well;
2012-12-31, by wenzelm
scala mode is already part of jedit-5.0.0;
2012-12-31, by wenzelm
tuned;
2012-12-31, by wenzelm
simplified quick start via "isabelle components -I";
2012-12-31, by wenzelm
tuned signature -- eliminated obsolete Standard_System;
2012-12-31, by wenzelm
tuned signature;
2012-12-31, by wenzelm
recovered generic PIDE build;
2012-12-31, by wenzelm
updated for release;
2012-12-31, by wenzelm
updated for release;
2012-12-31, by wenzelm
updated for release;
2012-12-31, by wenzelm
misc tuning for release;
2012-12-31, by wenzelm
recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
2012-12-31, by wenzelm
updated to smlnj-110.75;
2012-12-31, by wenzelm
tuned rendering;
2012-12-30, by wenzelm
ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
2012-12-30, by wenzelm
tuned;
2012-12-30, by wenzelm
more informative error;
2012-12-30, by wenzelm
tuned -- recovered comments from 791157a4179a;
2012-12-30, by wenzelm
tuned;
2012-12-30, by wenzelm
tuned whitespace;
2012-12-30, by wenzelm
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
2012-12-30, by wenzelm
tuned;
2012-12-29, by wenzelm
new theory Library/Finite_Lattice
2012-12-29, by nipkow
tuned ML function name
2012-12-28, by blanchet
slightly more elegant naming convention (to keep low-level and high-level APIs separated)
2012-12-28, by blanchet
tuned ML function names
2012-12-28, by blanchet
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
2012-12-28, by haftmann
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
2012-12-28, by haftmann
formally corrected
2012-12-28, by haftmann
tuned
2012-12-27, by haftmann
uniform parentheses for constructor -- necessary to accomodate scala 10
2012-12-27, by haftmann
more explicit name
2012-12-27, by haftmann
improved thm order hack, in case the default names are overridden
2012-12-27, by blanchet
enable theory learning in MaSh
2012-12-27, by blanchet
merged
2012-12-27, by blanchet
new version of MaSh
2012-12-27, by blanchet
fixed total
2012-12-27, by blanchet
new version of MaSh, with theory-level reasoning
2012-12-27, by blanchet
tuned
2012-12-27, by haftmann
prefer lxbroy10 to evade NFS/hg breakdown seen on various other local machines;
2012-12-26, by wenzelm
renamed and added lemmas
2012-12-23, by nipkow
added simp rule
2012-12-22, by nipkow
merged
2012-12-21, by nipkow
merged
2012-12-21, by nipkow
merged
2012-12-21, by nipkow
linearize eval driver, to work around horrible bug in previous implementation
2012-12-21, by blanchet
name tuning
2012-12-21, by blanchet
merge
2012-12-21, by blanchet
better weight functions for MePo/MaSh etc.
2012-12-20, by blanchet
merge
2012-12-20, by blanchet
more
2012-12-19, by blanchet
tuned infix table
2012-12-19, by nipkow
crank up default timeout for MaSh ATP learning
2012-12-19, by blanchet
removed odd associativity of ==
2012-12-19, by nipkow
updated SMT certificates
2012-12-21, by boehmes
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
2012-12-21, by boehmes
tuned "use build timeout": tuples cannot be concatenated
2012-12-20, by noschinl
use build timeout (wall clock time, default: 2h)
2012-12-19, by krauss
removed unused usedir_options
2012-12-19, by krauss
removed obsolete setting tweaks: build -s already sets output correctly
2012-12-19, by krauss
plain init_components calls instead of symlinks
2012-12-19, by krauss
tolerate non-existent ISABELLE_OUTPUT
2012-12-19, by krauss
removed obsolete parameter for contrib dir; hard-coding is not a problem
2012-12-19, by krauss
mira: do not hard-code polyml version
2012-12-19, by krauss
discontinued legacy antiquotations and styles
2012-12-18, by haftmann
avoid references altogether
2012-12-18, by blanchet
catch all parsing errors
2012-12-18, by blanchet
no need for tracing
2012-12-18, by blanchet
updated MaSh serialization number (to reflect new weights)
2012-12-17, by blanchet
synchronize access to shared reference and print proper total
2012-12-17, by blanchet
add a timeout in induction rule instantiation
2012-12-17, by blanchet
contain exponential explosion of term patterns
2012-12-17, by blanchet
tuned weights -- keep same relative values, but use 1.0 as the least weight
2012-12-17, by blanchet
really honor pattern depth, and use 2 by default
2012-12-17, by blanchet
tuned order to help debugging
2012-12-17, by blanchet
added table of infix operators
2012-12-17, by nipkow
made element and subset relations non-associative (just like all orderings)
2012-12-17, by nipkow
merged
2012-12-17, by wenzelm
more parallel find_unused_assms;
2012-12-17, by wenzelm
useful commutative diagram for while_option
2012-12-17, by traytel
more hints on technical issues due to shared-disk access of central Mercurial repository;
2012-12-17, by wenzelm
prefer implicit build_dialog of isabelle jedit;
2012-12-17, by wenzelm
offer sessions of group "main" first to increase chances that the user makes a sensible choice;
2012-12-17, by wenzelm
new contributor
2012-12-17, by nipkow
updated README;
2012-12-16, by wenzelm
HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
2012-12-16, by wenzelm
tuning
2012-12-16, by blanchet
merged
2012-12-16, by bulwahn
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
2012-12-16, by bulwahn
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
2012-12-16, by bulwahn
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
2012-12-16, by wenzelm
tuned property name;
2012-12-16, by wenzelm
allow to suppress ISABELLE_SYMBOLS for experiments;
2012-12-16, by wenzelm
escape nicknames
2012-12-16, by blanchet
generate proper nicks also for instantiated induction rules
2012-12-16, by blanchet
added tracing to ATP exporter
2012-12-16, by blanchet
merged
2012-12-15, by wenzelm
MaSh exporter can now export subsets of the facts, as consecutive ranges
2012-12-15, by blanchet
avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
2012-12-15, by blanchet
thread no timeout properly
2012-12-15, by blanchet
proper escaping in file name
2012-12-15, by blanchet
encode lemma name in file name
2012-12-15, by blanchet
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
2012-12-15, by wenzelm
prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;
2012-12-15, by wenzelm
maintain subtree_elements for improved performance of cumulate operator;
2012-12-15, by wenzelm
more formal class Markup_Tree.Elements;
2012-12-15, by wenzelm
tuned command line;
2012-12-15, by wenzelm
merged
2012-12-15, by wenzelm
unified layout of defs
2012-12-14, by nipkow
tuned;
2012-12-15, by wenzelm
clarified build_dialog command line;
2012-12-15, by wenzelm
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
2012-12-15, by wenzelm
updated README;
2012-12-15, by wenzelm
fold main goal;
2012-12-15, by wenzelm
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
2012-12-15, by wenzelm
tuned signature;
2012-12-15, by wenzelm
tuned;
2012-12-14, by wenzelm
tuned error dialog;
2012-12-14, by wenzelm
init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
2012-12-14, by wenzelm
more subgoal markup information, which is potentially useful to manage proof state output;
2012-12-14, by wenzelm
merged
2012-12-14, by nipkow
contribution by A. Colgio
2012-12-14, by nipkow
merged
2012-12-14, by nipkow
renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS
2012-12-13, by nipkow
actually request heap image in initial up-to-date check;
2012-12-14, by wenzelm
clarified "isabelle options" command line, to make it more close to "isabelle components";
2012-12-14, by wenzelm
updated some headers;
2012-12-14, by wenzelm
clarified README;
2012-12-14, by wenzelm
more formal components_checksum tool;
2012-12-14, by wenzelm
just one Admin/components/ directory;
2012-12-14, by wenzelm
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-14, by hoelzl
NEWS
2012-12-14, by hoelzl
merged
2012-12-14, by wenzelm
get rid of some junk facts in the MaSh evaluation driver
2012-12-13, by blanchet
generate original name as a comment in SPASS problems as well
2012-12-13, by blanchet
generate comments with original names for debugging
2012-12-13, by blanchet
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
2012-12-13, by blanchet
parallelized MaSh exporter
2012-12-13, by blanchet
short library for streams
2012-12-13, by traytel
renamed theory
2012-12-13, by traytel
renamed "emb" to "list_hembeq";
2012-12-13, by Christian Sternagel
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
2012-12-13, by blanchet
tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
2012-12-12, by blanchet
tuning
2012-12-12, by blanchet
tweaked which facts are included for MaSh evaluations
2012-12-12, by blanchet
don't query blacklisted theorems in evaluation driver
2012-12-12, by blanchet
export a pair of ML functions
2012-12-12, by blanchet
merged;
2012-12-14, by wenzelm
tuned implementation according to Library.insert/merge in ML;
2012-12-14, by wenzelm
more formal class Command.Results;
2012-12-14, by wenzelm
odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
2012-12-13, by wenzelm
smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13, by wenzelm
tuned;
2012-12-13, by wenzelm
enable Isabelle/ML to produce uninterpreted result messages as well;
2012-12-13, by wenzelm
include command results in tooltip as well;
2012-12-13, by wenzelm
more careful handling of Dialog_Result, with active area and color feedback;
2012-12-13, by wenzelm
identify dialogs via official serial and maintain as result message;
2012-12-13, by wenzelm
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-12-12, by wenzelm
support dialog via document content;
2012-12-12, by wenzelm
merged
2012-12-12, by wenzelm
further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"
2012-12-12, by blanchet
better tautology check -- don't reject "prod_cases3" for example
2012-12-12, by blanchet
tuned debugging file names
2012-12-12, by blanchet
more systematic identifier variants to facilitate experimentation;
2012-12-12, by wenzelm
prevent dedicated MacOSX plugin from switching off vital workarounds;
2012-12-12, by wenzelm
improved coupling of zoom_box and scale;
2012-12-12, by wenzelm
really all facts means really all facts (well, almost)
2012-12-12, by blanchet
tuning
2012-12-12, by blanchet
use modern SAT solvers with modern Kodkod versions
2012-12-12, by blanchet
got rid of support for Kodkodi < 1.2.14
2012-12-12, by blanchet
made MaSh evaluation driver work with SMT solvers
2012-12-12, by blanchet
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-12, by blanchet
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-12-12, by blanchet
better name for SMT solver files
2012-12-12, by blanchet
updated version of MaSh learner engine
2012-12-12, by blanchet
push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
2012-12-12, by blanchet
disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
2012-12-11, by wenzelm
less massive arrow heads;
2012-12-11, by wenzelm
added explicit zoom box;
2012-12-11, by wenzelm
some attempts at more discrete scale factor;
2012-12-11, by wenzelm
more official graphics context with font metrics;
2012-12-11, by wenzelm
just one class with parameters;
2012-12-11, by wenzelm
initial layout coordinates more like old browser;
2012-12-11, by wenzelm
added speculative options for jEdit;
2012-12-11, by wenzelm
separate instance of class Parameters for each Main_Panel -- avoid global program state;
2012-12-10, by wenzelm
discontinued long names flag -- better done via entity markup, without affecting layout;
2012-12-10, by wenzelm
tuned;
2012-12-10, by wenzelm
tuned;
2012-12-10, by wenzelm
tuned min/max;
2012-12-10, by wenzelm
tuned;
2012-12-10, by wenzelm
keep diagnostic command -- avoid confusion when it disappears;
2012-12-10, by wenzelm
tuned;
2012-12-10, by wenzelm
tuned signature;
2012-12-10, by wenzelm
removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;
2012-12-10, by wenzelm
merge
2012-12-10, by blanchet
merged
2012-12-10, by blanchet
merge
2012-12-10, by blanchet
changed capitalization of MeSh filter
2012-12-10, by blanchet
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
2012-12-10, by blanchet
further clarification for Windows;
2012-12-10, by wenzelm
merged
2012-12-10, by wenzelm
more generous tracing limit -- rescaled in MB;
2012-12-10, by wenzelm
recovered title property from bfb5964e3041;
2012-12-10, by wenzelm
some clarification for Windows;
2012-12-10, by wenzelm
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
2012-12-10, by wenzelm
tuned;
2012-12-10, by wenzelm
generalized notion of active area, where sendback is just one application;
2012-12-10, by wenzelm
merged
2012-12-10, by wenzelm
have MaSh evaluator keep all raw problem/solution files in a directory
2012-12-10, by blanchet
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
2012-12-10, by wenzelm
always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
2012-12-09, by wenzelm
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
2012-12-09, by wenzelm
merged
2012-12-08, by wenzelm
merge
2012-12-08, by blanchet
don't blacklist "case" theorems -- this causes problems in MaSh later
2012-12-08, by blanchet
more changes to MaSh Python program (by Daniel K.)
2012-12-08, by blanchet
don't have MaSh pretend it knows facts it doesn't know
2012-12-08, by blanchet
reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
2012-12-08, by blanchet
fixed embarrassing off-by-one bug in MaSh's Mesh
2012-12-08, by blanchet
store evaluation output in a file
2012-12-08, by blanchet
use parallel map
2012-12-08, by blanchet
tweak MaSh fudge factors
2012-12-08, by blanchet
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
2012-12-08, by blanchet
basic monitor panel, using the powerful jfreechart library;
2012-12-08, by wenzelm
added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);
2012-12-08, by wenzelm
check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
2012-12-08, by wenzelm
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
2012-12-07, by wenzelm
final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
2012-12-07, by wenzelm
adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;
2012-12-07, by wenzelm
obsolete;
2012-12-07, by wenzelm
eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
2012-12-07, by wenzelm
merged
2012-12-07, by wenzelm
deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;
2012-12-07, by wenzelm
some support to recover from spurious crash -- this is Physics, not Mathematics;
2012-12-07, by wenzelm
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
2012-12-07, by wenzelm
tuned text
2012-12-07, by nipkow
corrected nonsensical associativity of `` and dvd
2012-12-07, by nipkow
add exponential and uniform distributions
2012-12-07, by hoelzl
fundamental theorem of calculus for the Lebesgue integral
2012-12-07, by hoelzl
add Int_atMost
2012-12-07, by hoelzl
more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;
2012-12-07, by wenzelm
fork slow part of Thy_Load.body_files only;
2012-12-07, by wenzelm
explore theory_body_files via future, for improved performance;
2012-12-07, by wenzelm
merged
2012-12-06, by wenzelm
use proper entry point for MaSh in test driver
2012-12-06, by blanchet
export ATP and Isar commands separately
2012-12-06, by blanchet
proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
2012-12-06, by wenzelm
discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
2012-12-06, by wenzelm
discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;
2012-12-06, by wenzelm
updated README;
2012-12-06, by wenzelm
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
2012-12-06, by wenzelm
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
2012-12-06, by wenzelm
avoid startup within GUI thread -- it is only required later for dialog;
2012-12-06, by wenzelm
more uniform default logic, using settings, options, args etc.;
2012-12-06, by wenzelm
use right names in MePo exporter
2012-12-06, by blanchet
parse more liberal MaSh suggestion syntax (for the eval driver)
2012-12-06, by blanchet
merged
2012-12-06, by wenzelm
made Python code compile again (by Daniel K.)
2012-12-06, by blanchet
tweaked MaSh proximity
2012-12-06, by blanchet
reduce max number of dependencies for MaSh to get rid of junk
2012-12-06, by blanchet
more feature tweaks
2012-12-06, by blanchet
prioritize chained facts
2012-12-06, by blanchet
more MaSh feature tweaking
2012-12-06, by blanchet
record free variables as a MaSh feature
2012-12-06, by blanchet
expand type classes into their ancestors for MaSh
2012-12-06, by blanchet
tweaked MaSh features, based on comments by Josef Urban
2012-12-06, by blanchet
increase weight of local facts again (MaSh)
2012-12-06, by blanchet
simplify code now that "mash.py" supports weights
2012-12-06, by blanchet
added weights to MaSh (by Daniel Kuehlwein)
2012-12-06, by blanchet
Move the measurability prover to its own file
2012-12-05, by hoelzl
Show search depth in the debug output of the measurability prover
2012-12-05, by hoelzl
Remove looping rule from measurability prover
2012-12-05, by hoelzl
rules for improper Lebesgue integrals (using tendsto at_top)
2012-12-04, by hoelzl
take proximity into account for MaSh + fix a debilitating bug in feature generation
2012-12-05, by blanchet
tuning
2012-12-05, by blanchet
clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);
2012-12-06, by wenzelm
select logic session names, not paths;
2012-12-05, by wenzelm
added keyboard shortcut for button (canonical way to do that?);
2012-12-05, by wenzelm
evade ugly default font, notably on Windows laf;
2012-12-05, by wenzelm
center main window;
2012-12-05, by wenzelm
more direct dialog via existing GUI components;
2012-12-05, by wenzelm
clarified logic argument: session name, not path name;
2012-12-05, by wenzelm
tuned message;
2012-12-05, by wenzelm
implicit build_dialog for Isabelle/jEdit;
2012-12-05, by wenzelm
tuned message;
2012-12-05, by wenzelm
tuned OK feedback;
2012-12-05, by wenzelm
check for existing image (even if outdated);
2012-12-05, by wenzelm
more elementary dialog, with less interaction;
2012-12-05, by wenzelm
basic interaction with build process;
2012-12-05, by wenzelm
allow to terminate jobs via Progress;
2012-12-05, by wenzelm
more formal progress context;
2012-12-05, by wenzelm
basic wrapper for session build dialog;
2012-12-05, by wenzelm
tuned;
2012-12-05, by wenzelm
tuned signature in accordance to document operations;
2012-12-05, by wenzelm
tuned;
2012-12-05, by wenzelm
merged
2012-12-05, by nipkow
\<noteq> now has the same associativity as ~= and =
2012-12-05, by nipkow
tweaked order of theorems to avoid forward dependencies (MaSh)
2012-12-05, by blanchet
rationalized MaSh evaluation harness
2012-12-04, by blanchet
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
2012-12-04, by blanchet
added feature weights in MaSh
2012-12-04, by blanchet
promote local facts using a hack (for MaSh)
2012-12-04, by blanchet
proper action labels, to make this appear in the "Shortcuts" panel, for example;
2012-12-04, by wenzelm
turned off noisy MaSh features
2012-12-04, by blanchet
added MaSh learning to Mirabelle
2012-12-04, by blanchet
fixed bug in initialization of naive Bayes (MaSh)
2012-12-04, by blanchet
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
2012-12-04, by blanchet
generalized MaSh exporter to sets of theories
2012-12-04, by blanchet
remove SMT proofs in Multivariate_Analysis
2012-12-04, by hoelzl
prove tendsto_power_div_exp_0
2012-12-04, by hoelzl
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
2012-12-04, by hoelzl
merged
2012-12-04, by wenzelm
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
2012-12-04, by wenzelm
go back to Z3 3.2
2012-12-04, by blanchet
tuned defs of sec_xyz
2012-12-04, by nipkow
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
2012-12-04, by wenzelm
simplify MaSh term patterns + add missing global facts if there aren't too many
2012-12-04, by blanchet
MaSh improvements: deeper patterns + more respect for chained facts
2012-12-04, by blanchet
tuned names
2012-12-03, by blanchet
tweaked MaSh exporter
2012-12-03, by blanchet
renamed "Type.thy" to something that's less likely to cause conflicts
2012-12-03, by blanchet
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
2012-12-03, by blanchet
added "fact_filter" option to Mirabelle
2012-12-03, by blanchet
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
2012-12-03, by blanchet
some notes on the Isabelle component repository at TUM;
2012-12-03, by wenzelm
use filterlim in Lim and SEQ; tuned proofs
2012-12-03, by hoelzl
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
2012-12-03, by hoelzl
weakened assumptions for lhopital_right_0
2012-12-03, by hoelzl
tuned proof
2012-12-03, by hoelzl
add L'Hôpital's rule
2012-12-03, by hoelzl
add filterlim rules for exp and ln to infinity
2012-12-03, by hoelzl
add filterlim rules for inverse and at_infinity
2012-12-03, by hoelzl
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
2012-12-03, by hoelzl
add filterlim rules for unary minus and inverse
2012-12-03, by hoelzl
rename filter_lim to filterlim to be consistent with filtermap
2012-12-03, by hoelzl
add check to Cooper's algorithm that left-hand of dvd is a numeral
2012-12-03, by hoelzl
merged
2012-12-03, by wenzelm
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
2012-12-03, by blanchet
avoid odd warnings due to failure of systray icon;
2012-12-03, by wenzelm
synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
2012-12-03, by wenzelm
tuned;
2012-12-03, by wenzelm
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
2012-12-03, by wenzelm
semi-automated Cygwin setup;
2012-12-02, by wenzelm
misc tuning;
2012-12-02, by wenzelm
updated to sumatra_pdf-2.1.1;
2012-12-02, by wenzelm
tuned order of functions
2012-12-01, by blanchet
proper quoting of paths in MaSh
2012-12-01, by blanchet
updated to jedit_build-20121201 (based on jedit-5.0.0);
2012-12-01, by wenzelm
moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
2012-12-01, by wenzelm
leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;
2012-12-01, by wenzelm
updated to jedit-5.0.0;
2012-12-01, by wenzelm
more generic directory name to facilitate tracking changes of diffs;
2012-12-01, by wenzelm
merged
2012-11-30, by wenzelm
tuned
2012-11-30, by nipkow
added 'print_inductives' command;
2012-11-30, by wenzelm
print formal entities with markup;
2012-11-30, by wenzelm
tuned labels;
2012-11-30, by wenzelm
renamed dockable "Prover Session" to "Theories";
2012-11-30, by wenzelm
tuned import;
2012-11-30, by wenzelm
alternative shortcut for English keyboard;
2012-11-30, by wenzelm
merged
2012-11-30, by wenzelm
eliminated redundant is_ident -- more official is_identifier;
2012-11-30, by wenzelm
updated to jdk-7u9;
2012-11-30, by wenzelm
updated to exec_process-1.0.3;
2012-11-30, by wenzelm
report proper pid *after* fork;
2012-11-30, by wenzelm
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
2012-11-30, by wenzelm
more defensive retry via fork;
2012-11-29, by wenzelm
merged
2012-11-29, by wenzelm
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
2012-11-29, by kuncar
simplified use of fold/map;
2012-11-29, by wenzelm
tuned;
2012-11-29, by wenzelm
prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);
2012-11-29, by wenzelm
merged
2012-11-29, by wenzelm
make SML/NJ happy (give names for all fields in a record)
2012-11-29, by hoelzl
more robust syntax that survives collapse of \<^isub> and \<^sub>;
2012-11-29, by wenzelm
further update and clarification of the all-important README_REPOSITORY;
2012-11-29, by wenzelm
more uniform ML statistics;
2012-11-29, by wenzelm
merged
2012-11-28, by wenzelm
improved readability
2012-11-28, by smolkas
tweaked calculation of sledgehammer messages
2012-11-28, by smolkas
adapted sledgehammer warnings
2012-11-28, by smolkas
fixed case split preplaying
2012-11-28, by smolkas
fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup
2012-11-28, by smolkas
preplay case splits
2012-11-28, by smolkas
added warning when shrinking proof without preplaying
2012-11-28, by smolkas
deal with the case that metis does not time out, but fails instead
2012-11-28, by smolkas
reapplied changes to make SML/NJ happy
2012-11-28, by smolkas
renaming, minor tweaks, added signature
2012-11-28, by smolkas
added signature
2012-11-28, by smolkas
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
2012-11-28, by smolkas
removed duplicate decleration
2012-11-28, by smolkas
made use of sledgehammer_util
2012-11-28, by smolkas
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
2012-11-28, by smolkas
added comments to new source files
2012-11-28, by smolkas
fixed problem with fact names
2012-11-28, by smolkas
remove hack and generalize code slightly
2012-11-28, by smolkas
simplified isar_qualifiers and qs merging
2012-11-28, by smolkas
put shrink in own structure
2012-11-28, by smolkas
put annotate in own structure
2012-11-28, by smolkas
support assumptions as facts for preplaying
2012-11-28, by smolkas
some minor improvements in shrink_proof
2012-11-28, by smolkas
some support for ML runtime statistics;
2012-11-28, by wenzelm
prefer tight Markup.print_int/parse_int for property values;
2012-11-28, by wenzelm
clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
2012-11-28, by wenzelm
eliminated slightly odd identifiers;
2012-11-28, by wenzelm
tuned syntax, potentially more robust;
2012-11-28, by wenzelm
smarter list layout;
2012-11-28, by wenzelm
repaired text following 491c5c81c2e8;
2012-11-27, by wenzelm
merged
2012-11-27, by wenzelm
introduce filter_lim as a generatlization of tendsto
2012-11-27, by hoelzl
merged
2012-11-27, by wenzelm
based countable topological basis on Countable_Set
2012-11-27, by immler
qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-27, by immler
eliminated finite_set_sequence with countable set
2012-11-22, by immler
support for sub-structured identifier syntax (inactive);
2012-11-27, by wenzelm
eliminated some improper identifiers;
2012-11-27, by wenzelm
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
2012-11-27, by hoelzl
tuned signature;
2012-11-26, by wenzelm
more uniform Symbol.is_ascii_identifier in ML/Scala;
2012-11-26, by wenzelm
tuned;
2012-11-26, by wenzelm
clarified Symbol.scan_ascii_id;
2012-11-26, by wenzelm
tuned;
2012-11-26, by wenzelm
convenience operations for table as set;
2012-11-26, by wenzelm
removed remains of Oheimb's double-space (cf. 0a5af667dc75);
2012-11-26, by wenzelm
tuned;
2012-11-26, by wenzelm
merged
2012-11-26, by wenzelm
updated two components
2012-11-26, by blanchet
simplify code slightly
2012-11-26, by blanchet
avoid non-ASCII sign
2012-11-26, by blanchet
generate a parameterized correspondence relation
2012-11-26, by kuncar
quot_thm_crel
2012-11-26, by kuncar
add option_fold
2012-11-26, by kuncar
add binomial_ge_n_over_k_pow_k
2012-11-26, by hoelzl
removed tool that was never finished
2012-11-26, by blanchet
added file headers
2012-11-26, by blanchet
updated MaSh doc
2012-11-26, by blanchet
moved MaSh's Python code into Isabelle
2012-11-26, by blanchet
updated NEWS etc.
2012-11-26, by blanchet
distinguish declated tfrees from other tfrees -- only the later can be optimized away
2012-11-26, by blanchet
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
2012-11-26, by wenzelm
reset active areas on content update;
2012-11-26, by wenzelm
more general sendback properties;
2012-11-26, by wenzelm
tuned command descriptions;
2012-11-26, by wenzelm
refined outer syntax 'help' command;
2012-11-26, by wenzelm
tuned signature;
2012-11-26, by wenzelm
always reset active areas;
2012-11-26, by wenzelm
no special treatment of control_reset, in accordance to other control styles;
2012-11-26, by wenzelm
tuned signature;
2012-11-25, by wenzelm
tuned signature;
2012-11-25, by wenzelm
tuned signature;
2012-11-25, by wenzelm
tuned signature;
2012-11-25, by wenzelm
renamed main plugin object to PIDE;
2012-11-25, by wenzelm
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
2012-11-25, by wenzelm
explicit module UTF8;
2012-11-25, by wenzelm
tuned file name;
2012-11-25, by wenzelm
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-25, by wenzelm
prefer strict error;
2012-11-25, by wenzelm
quasi-abstract module Rendering, with Isabelle-specific implementation;
2012-11-25, by wenzelm
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
2012-11-25, by wenzelm
eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
2012-11-25, by wenzelm
retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;
2012-11-24, by wenzelm
prefer buffer_edit combinator over Java-style boilerplate;
2012-11-24, by wenzelm
more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
2012-11-24, by wenzelm
tuned symbol groups;
2012-11-24, by wenzelm
tuned -- Symbol.groups already sorted;
2012-11-24, by wenzelm
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
2012-11-24, by wenzelm
added option jedit_symbols_search_limit;
2012-11-24, by wenzelm
avoid empty tooltip;
2012-11-24, by wenzelm
tuned symbol groups;
2012-11-24, by wenzelm
special handling of control symbols in Symbols dockable;
2012-11-24, by wenzelm
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
2012-11-24, by wenzelm
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
2012-11-24, by wenzelm
more NEWS/CONTRIBUTORS;
2012-11-24, by wenzelm
improved editing support for control styles;
2012-11-24, by wenzelm
added ISABELLE_PLATFORM_FAMILY;
2012-11-24, by wenzelm
merged
2012-11-23, by nipkow
moved lemma
2012-11-23, by nipkow
timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
2012-11-23, by wenzelm
add quotient_of_div
2012-11-23, by hoelzl
generate correct names
2012-11-23, by kuncar
simplified code
2012-11-23, by kuncar
generate correct correspondence relation name
2012-11-23, by kuncar
more uniform title, follow-up to 928cb8b35e6e;
2012-11-23, by wenzelm
tuned
2012-11-23, by nipkow
defer interpretation of markup via implicit print mode;
2012-11-22, by wenzelm
merged
2012-11-22, by wenzelm
made SML/NJ happier
2012-11-22, by traytel
pack window before accessing its geometry;
2012-11-22, by wenzelm
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
2012-11-22, by wenzelm
more precise tooltip window size;
2012-11-22, by wenzelm
take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;
2012-11-22, by wenzelm
reset active area for outdated snapshot (again?);
2012-11-22, by wenzelm
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
2012-11-22, by wenzelm
more abstract Sendback operations, with explicit id/exec_id properties;
2012-11-22, by wenzelm
some support for breakable text and paragraphs;
2012-11-22, by wenzelm
tuned names
2012-11-22, by nipkow
tuned comment;
2012-11-21, by wenzelm
clarified symbol groups, despite this traditional arrangement in X-symbol grid;
2012-11-21, by wenzelm
always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
2012-11-21, by wenzelm
tuned whitespace;
2012-11-21, by wenzelm
merged
2012-11-21, by immler
included abbrev in tooltip
2012-11-21, by immler
removed (unicode) tooltips: can not adjust font in basic swing tooltip
2012-11-21, by immler
delayed search to improve reactivity
2012-11-21, by immler
respect font property for symbols
2012-11-21, by immler
capitalize lowercase groups;
2012-11-21, by immler
merged
2012-11-21, by wenzelm
more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
2012-11-21, by wenzelm
Countable_Set: tuned lemma names; more generic lemmas
2012-11-21, by hoelzl
enable Symbols dockable by default;
2012-11-21, by wenzelm
tuned;
2012-11-21, by wenzelm
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
2012-11-21, by wenzelm
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
2012-11-21, by hoelzl
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
2012-11-21, by immler
CONTRIBUTION: add fabians work
2012-11-21, by hoelzl
NEWS: document changes in HOL-Probability
2012-11-21, by hoelzl
NEWS (changeset 13211e07d931): add Countable_Set
2012-11-21, by hoelzl
NEWS (changeset 69b35a75caf3): document changes in FuncSet
2012-11-21, by hoelzl
new theory of immutable arrays
2012-11-21, by nipkow
some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
2012-11-20, by wenzelm
support for symbol groups, retaining original order of declarations;
2012-11-20, by wenzelm
tuned;
2012-11-20, by wenzelm
add Countable_Set theory
2012-11-20, by hoelzl
tuned proof
2012-11-20, by nipkow
simplified command line of "isabelle install";
2012-11-20, by wenzelm
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
2012-11-20, by wenzelm
some documentation for "algebra" in HOL;
2012-11-20, by wenzelm
global default for session timeout;
2012-11-20, by wenzelm
alternative completion for outer syntax keywords;
2012-11-19, by wenzelm
init options on startup as well;
2012-11-19, by wenzelm
theorem status about oracles/futures is no longer printed by default;
2012-11-19, by wenzelm
tuned: use induction rule sigma_sets_induct_disjoint
2012-11-19, by hoelzl
tuned FinMap
2012-11-19, by hoelzl
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-19, by hoelzl
more refs;
2012-11-19, by wenzelm
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
2012-11-18, by wenzelm
proper jvmpath for windows;
2012-11-18, by wenzelm
more generous tracing_limit, with explicit system option;
2012-11-18, by wenzelm
adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
2012-11-18, by wenzelm
update options via protocol;
2012-11-18, by wenzelm
more accurate pixel_range -- do not round offset here;
2012-11-18, by wenzelm
tuned signature;
2012-11-18, by wenzelm
prefer absolute default $USER_HOME/Scratch.thy;
2012-11-17, by wenzelm
more portable process exit;
2012-11-17, by wenzelm
tuned -- eliminate pointless ML method definition;
2012-11-17, by wenzelm
tuned;
2012-11-17, by wenzelm
NEWS;
2012-11-17, by wenzelm
tuned structure of Isabelle/HOL;
2012-11-17, by wenzelm
method setup for Classical steps;
2012-11-17, by wenzelm
tuned signature;
2012-11-17, by wenzelm
updated keywords;
2012-11-17, by wenzelm
moved (b)choice_iff(') to Hilbert_Choice
2012-11-16, by hoelzl
move theorems to be more generally useable
2012-11-16, by hoelzl
merged
2012-11-16, by wenzelm
made SML/NJ happy;
2012-11-16, by wenzelm
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
2012-11-16, by hoelzl
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
2012-11-16, by hoelzl
measurability for nat_case and comb_seq
2012-11-16, by hoelzl
rules for AE and prob
2012-11-16, by hoelzl
rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication
2012-11-16, by hoelzl
more measurability rules
2012-11-16, by hoelzl
renamed to more appropriate lim_P for projective limit
2012-11-16, by immler
allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-16, by immler
repaired slip accidentally introduced in 57209cfbf16b
2012-11-15, by haftmann
prefer implementation in HOL;
2012-11-15, by haftmann
corrected headers
2012-11-15, by immler
hide constants of auxiliary type finmap
2012-11-15, by immler
generalized to copy of countable types instead of instantiation of nat for discrete topology
2012-11-15, by immler
added projective limit;
2012-11-15, by immler
regularity of measures, therefore:
2012-11-15, by immler
tuned -- eliminated obsolete citation of isabelle-ref;
2012-11-15, by wenzelm
updated basic equality rules;
2012-11-12, by wenzelm
removed somewhat pointless historic material;
2012-11-12, by wenzelm
updated unification options;
2012-11-11, by wenzelm
removed some historic material that is obsolete or rarely used;
2012-11-11, by wenzelm
tuned;
2012-11-11, by wenzelm
updated section on ordered rewriting;
2012-11-11, by wenzelm
updated subgoaler/solver/looper;
2012-11-10, by wenzelm
removed somewhat pointless historic material;
2012-11-08, by wenzelm
tuned;
2012-11-08, by wenzelm
updated explanation of rewrite rules;
2012-11-08, by wenzelm
(re)moved old material about Simplifier;
2012-11-07, by wenzelm
some coverage of "resolution without lifting", which should be normally avoided;
2012-11-07, by wenzelm
removed somewhat pointless historic material;
2012-11-07, by wenzelm
updated biresolve_tac, bimatch_tac;
2012-11-07, by wenzelm
moved classical wrappers to IsarRef;
2012-11-07, by wenzelm
avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");
2012-11-04, by wenzelm
updated citations;
2012-11-04, by wenzelm
tuned;
2012-11-04, by wenzelm
removed junk;
2012-11-04, by wenzelm
removed pointless historic material;
2012-11-04, by wenzelm
more on Simplifier rules, based on old material;
2012-11-04, by wenzelm
refurbished Simplifier examples;
2012-11-04, by wenzelm
more on the Simplifier, based on old material;
2012-11-03, by wenzelm
more concise/precise documentation;
2012-11-03, by wenzelm
tuned text
2012-11-14, by nipkow
replaced relation by function - simplifies development
2012-11-14, by nipkow
made SMLNJ happier
2012-11-13, by traytel
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
2012-11-13, by traytel
prefer explicit Random.seed
2012-11-13, by haftmann
dropped dead code
2012-11-12, by haftmann
tuned import order
2012-11-12, by haftmann
tuned layout
2012-11-12, by nipkow
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
2012-11-12, by blanchet
create temp directory if not already created
2012-11-12, by blanchet
merged
2012-11-12, by nipkow
new theory IMP/Finite_Reachable
2012-11-12, by nipkow
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
2012-11-12, by blanchet
centralized term printing code
2012-11-12, by blanchet
thread context correctly when printing backquoted facts
2012-11-12, by blanchet
dropped dead code;
2012-11-11, by haftmann
modernized, simplified and compacted oracle and proof method glue code;
2012-11-11, by haftmann
merged
2012-11-09, by nipkow
fixed underscores
2012-11-09, by nipkow
moved lemmas into projective_family; added header for theory Projective_Family
2012-11-09, by immler
removed redundant/unnecessary assumptions from projective_family
2012-11-09, by immler
assume probability spaces; allow empty index set
2012-11-07, by immler
added projective_family; generalized generator in product_prob_space to projective_family
2012-11-07, by immler
moved lemmas further up
2012-11-06, by immler
tuned proofs
2012-11-08, by bulwahn
using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier
2012-11-08, by bulwahn
hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
2012-11-08, by bulwahn
NEWS
2012-11-08, by bulwahn
rewriting with the simpset that is passed to the simproc
2012-11-08, by bulwahn
handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc
2012-11-08, by bulwahn
tuned
2012-11-08, by bulwahn
syntactic tuning and restructuring of set_comprehension_pointfree simproc
2012-11-08, by bulwahn
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
2012-11-08, by bulwahn
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
2012-11-08, by bulwahn
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-11-08, by bulwahn
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
2012-11-08, by bulwahn
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
2012-11-08, by bulwahn
simplified structure of patterns in set_comprehension_simproc
2012-11-08, by bulwahn
refined stack of library theories implementing int and/or nat by target language numerals
2012-11-08, by haftmann
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
2012-11-07, by haftmann
add support for function application to measurability prover
2012-11-06, by hoelzl
renamed Sledgehammer option
2012-11-06, by blanchet
always show timing for structured proofs
2012-11-06, by blanchet
use implications rather than disjunctions to improve readability
2012-11-06, by blanchet
avoid name clashes
2012-11-06, by blanchet
fixed more "Trueprop" issues
2012-11-06, by blanchet
removed needless sort
2012-11-06, by blanchet
avoid double "Trueprop"s
2012-11-06, by blanchet
use original formulas for hypotheses and conclusion to avoid mismatches
2012-11-06, by blanchet
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
2012-11-06, by blanchet
correct parsing of E dependencies
2012-11-06, by blanchet
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
2012-11-06, by blanchet
tuned
2012-11-05, by nipkow
code for while directly, not via while_option
2012-11-04, by nipkow
executable true liveness analysis incl an approximating version
2012-11-04, by nipkow
now that sets are executable again, no more special treatment of variable sets
2012-11-04, by nipkow
handle non-unit clauses gracefully
2012-11-02, by blanchet
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
2012-11-02, by blanchet
use measurability prover
2012-11-02, by hoelzl
add measurability prover; add support for Borel sets
2012-11-02, by hoelzl
add syntax and a.e.-rules for (conditional) probability on predicates
2012-11-02, by hoelzl
infinite product measure is invariant under adding prefixes
2012-11-02, by hoelzl
for the product measure it is enough if only one measure is sigma-finite
2012-11-02, by hoelzl
Allow parentheses around left-hand sides of array associations
2012-11-02, by berghofe
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
2012-11-01, by blanchet
regenerated SMT certificates
2012-11-01, by blanchet
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
2012-11-01, by blanchet
fixed bool vs. prop mismatch
2012-10-31, by blanchet
removed "refute" command from Isar manual, now that it has been moved outside "Main"
2012-10-31, by blanchet
repaired "Mutabelle" after Refute move
2012-10-31, by blanchet
less verbose -- the warning will reach the users anyway by other means
2012-10-31, by blanchet
tuned messages
2012-10-31, by blanchet
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-10-31, by blanchet
fixes related to Refute's move
2012-10-31, by blanchet
added a timeout around script that relies on the network
2012-10-31, by blanchet
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
2012-10-31, by blanchet
moved Refute to "HOL/Library" to speed up building "Main" even more
2012-10-31, by blanchet
tuning
2012-10-31, by blanchet
use metaquantification when possible in Isar proofs
2012-10-31, by blanchet
tuned code
2012-10-31, by blanchet
tuning
2012-10-31, by blanchet
soft SMT timeout
2012-10-31, by blanchet
added function store_termination_rule to the signature, as it is used in Nominal2
2012-10-28, by Christian Urban
longer log, to accomodate final status line of isabelle build;
2012-10-27, by wenzelm
transfer package: error message if preprocessing goal to object-logic formula fails
2012-10-24, by huffman
transfer package: add test to prevent trying to make cterms from open terms
2012-10-24, by huffman
transfer package: more flexible handling of equality relations using is_equality predicate
2012-10-24, by huffman
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
2012-10-24, by nipkow
new theorems
2012-10-22, by kuncar
incorporated constant chars into instantiation proof for enum;
2012-10-22, by haftmann
close code theorems explicitly after preprocessing
2012-10-22, by haftmann
tuned proofs;
2012-10-22, by wenzelm
further attempts to cope with large files via option jedit_text_overview_limit;
2012-10-22, by wenzelm
more detailed Prover IDE NEWS;
2012-10-22, by wenzelm
recovered explicit error message, which was lost in b8570ea1ce25;
2012-10-21, by wenzelm
removed dead code;
2012-10-21, by wenzelm
proper signatures;
2012-10-21, by wenzelm
tuned;
2012-10-21, by wenzelm
merged
2012-10-21, by webertj
Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-19, by webertj
Tuned.
2012-10-19, by webertj
more conventional argument order;
2012-10-21, by haftmann
another refinement in the comprehension conversion
2012-10-21, by bulwahn
refined simplifier call in comprehension_conv
2012-10-21, by bulwahn
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
2012-10-21, by bulwahn
avoid STIX font, which tends to render badly;
2012-10-20, by wenzelm
extra jar for scala-2.10.0-RC1;
2012-10-20, by wenzelm
more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
2012-10-20, by wenzelm
avoid duplicate build of jars_fresh;
2012-10-20, by wenzelm
obsolete, cf. README_REPOSITORY;
2012-10-20, by wenzelm
accomodate scala-2.10.0-RC1;
2012-10-20, by wenzelm
tailored enum specification towards simple instantiation;
2012-10-20, by haftmann
refined internal structure of Enum.thy
2012-10-20, by haftmann
moved quite generic material from theory Enum to more appropriate places
2012-10-20, by haftmann
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
2012-10-20, by bulwahn
improving tactic in setcomprehension_simproc
2012-10-20, by bulwahn
adjusting proofs
2012-10-20, by bulwahn
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
2012-10-20, by bulwahn
passing names and types of all bounds around in the simproc
2012-10-20, by bulwahn
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
2012-10-18, by bulwahn
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
2012-10-19, by wenzelm
merged
2012-10-19, by wenzelm
don't include Quotient_Option - workaround to a transfer bug
2012-10-19, by kuncar
ignore old stuff and thus speed up the script greatly;
2012-10-19, by wenzelm
proper find -mtime (file data) instead of -ctime (meta data);
2012-10-19, by wenzelm
made SML/NJ happy;
2012-10-19, by wenzelm
clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);
2012-10-19, by wenzelm
back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;
2012-10-18, by wenzelm
merged
2012-10-18, by wenzelm
back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
2012-10-18, by wenzelm
more basic Goal.reset_futures as snapshot of implicit state;
2012-10-18, by wenzelm
tuned proof;
2012-10-18, by wenzelm
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
2012-10-18, by kuncar
tuned proofs
2012-10-18, by kuncar
new theorem
2012-10-18, by kuncar
merged
2012-10-18, by wenzelm
merged
2012-10-18, by wenzelm
merged
2012-10-18, by wenzelm
merged
2012-10-18, by wenzelm
fixed proof (cf. a81f95693c68);
2012-10-18, by wenzelm
tuned Isar output
2012-10-18, by blanchet
tuned
2012-10-18, by nipkow
updated docs
2012-10-18, by blanchet
renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18, by blanchet
tuning
2012-10-18, by blanchet
fixed theorem lookup code in Isar proof reconstruction
2012-10-18, by blanchet
tuning
2012-10-18, by blanchet
refactor code
2012-10-18, by blanchet
tuning
2012-10-18, by blanchet
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
2012-10-18, by wenzelm
collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
2012-10-18, by wenzelm
more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;
2012-10-18, by wenzelm
tuned message;
2012-10-18, by wenzelm
tuned comment;
2012-10-18, by wenzelm
avoid spurious "bad" markup for show/test_proof;
2012-10-18, by wenzelm
more official Future.terminate;
2012-10-18, by wenzelm
simp results for simplification results of Inf/Sup expressions on bool;
2012-10-18, by haftmann
no sort constraints on datatype constructors in internal bookkeeping
2012-10-18, by haftmann
HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);
2012-10-17, by wenzelm
merged
2012-10-17, by wenzelm
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
2012-10-17, by bulwahn
checking for bound variables in the set expression; handling negation more generally
2012-10-17, by bulwahn
set_comprehension_pointfree simproc now handles the complicated test case; tuned
2012-10-17, by bulwahn
refined conversion to only react on proper set comprehensions; tuned
2012-10-17, by bulwahn
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
2012-10-17, by bulwahn
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
2012-10-17, by bulwahn
another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);
2012-10-17, by wenzelm
more robust cancel_now: avoid shooting yourself in the foot;
2012-10-17, by wenzelm
more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
2012-10-17, by wenzelm
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
2012-10-17, by wenzelm
added Output "Detach" button;
2012-10-17, by wenzelm
skipped proofs appear as "bad" without counting as error;
2012-10-17, by wenzelm
more method position information, notably finished_pos after end of previous text;
2012-10-17, by wenzelm
more formal markup;
2012-10-17, by wenzelm
tuned signature;
2012-10-17, by wenzelm
more formal markup;
2012-10-17, by wenzelm
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
2012-10-17, by kuncar
merged
2012-10-16, by wenzelm
added missing file
2012-10-16, by blanchet
tuned for document output
2012-10-16, by traytel
added proof minimization code from Steffen Smolka
2012-10-16, by blanchet
tuned blank lines
2012-10-16, by traytel
tuned whitespace
2012-10-16, by traytel
a few notations changed in HOL/BNF/Examples/Derivation_Trees
2012-10-16, by popescua
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
2012-10-16, by popescua
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
2012-10-16, by bulwahn
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
2012-10-16, by bulwahn
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
2012-10-16, by bulwahn
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
2012-10-16, by bulwahn
update ROOT with teh directory change in BNF
2012-10-16, by popescua
changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees
2012-10-16, by popescua
retain info dockable state via educated guess on window focus;
2012-10-16, by wenzelm
support for more informative errors in lazy enumerations;
2012-10-16, by wenzelm
more informative errors for 'also' and 'finally';
2012-10-16, by wenzelm
tuned messages;
2012-10-16, by wenzelm
more proof method text position information;
2012-10-16, by wenzelm
clarified defer/prefer: more specific errors;
2012-10-16, by wenzelm
updated Toplevel.proofs;
2012-10-16, by wenzelm
more informative errors for 'proof' and 'apply' steps;
2012-10-16, by wenzelm
more friendly handling of Pure.thy bootstrap errors;
2012-10-16, by wenzelm
more informative error for stand-alone 'qed';
2012-10-16, by wenzelm
further attempts to unify/simplify goal output;
2012-10-16, by wenzelm
more informative error messages of initial/terminal proof methods;
2012-10-16, by wenzelm
merged
2012-10-15, by wenzelm
setcomprehension_pointfree simproc also works for set comprehension without an equation
2012-10-15, by bulwahn
tuned message -- avoid extra blank lines;
2012-10-15, by wenzelm
updated to polyml-5.5.0 which reduces chance of HOL-IMP failure (although it is hard to reproduce anyway);
2012-10-15, by wenzelm
store colors after build
2012-10-14, by Markus Kaiser
adding further test cases for the set_comprehension_pointfree simproc
2012-10-14, by bulwahn
refined tactic in set_comprehension_pointfree simproc
2012-10-14, by bulwahn
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
2012-10-14, by bulwahn
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
2012-10-14, by bulwahn
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
2012-10-14, by bulwahn
more informative error of initial/terminal proof steps;
2012-10-13, by wenzelm
some attempts to unify/simplify pretty_goal;
2012-10-13, by wenzelm
refined Proof.the_finished_goal with more informative error;
2012-10-13, by wenzelm
tuned signature;
2012-10-13, by wenzelm
improved adhoc height for small fonts;
2012-10-13, by wenzelm
further refinement of jEdit line range, avoiding lack of final \n;
2012-10-12, by wenzelm
more uniform tooltip color;
2012-10-12, by wenzelm
more NEWS;
2012-10-12, by wenzelm
merged
2012-10-12, by wenzelm
disambiguated grammar
2012-10-12, by traytel
tuned proofs
2012-10-12, by traytel
tuned
2012-10-12, by nipkow
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
2012-10-12, by wenzelm
discontinued typedef with alternative name;
2012-10-12, by wenzelm
discontinued obsolete typedef (open) syntax;
2012-10-12, by wenzelm
discontinued typedef with implicit set_def;
2012-10-12, by wenzelm
merged
2012-10-12, by wenzelm
increading indexes to avoid clashes in the set_comprehension_pointfree simproc
2012-10-12, by bulwahn
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
2012-10-12, by wenzelm
do not treat interrupt as error here, to avoid confusion in log etc.;
2012-10-12, by wenzelm
more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
2012-10-12, by wenzelm
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-10-11, by wenzelm
merged
2012-10-11, by wenzelm
cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-11, by hoelzl
msetprod based directly on Multiset.fold;
2012-10-11, by haftmann
avoid global interpretation
2012-10-11, by haftmann
simplified construction of fold combinator on multisets;
2012-10-11, by haftmann
clarified output token markup (see also bc22daeed49e);
2012-10-11, by wenzelm
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
2012-10-11, by wenzelm
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
more position information for hyperlink and placement of message;
2012-10-11, by wenzelm
tuned;
2012-10-11, by wenzelm
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
2012-10-11, by krauss
removed unused legacy material from mira.py
2012-10-10, by krauss
eliminated some remaining uses of typedef with implicit set definition;
2012-10-10, by wenzelm
merged
2012-10-10, by Andreas Lochbihler
fix code equation for RBT_Impl.fold
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by Andreas Lochbihler
tail-recursive implementation for length
2012-10-10, by Andreas Lochbihler
correct definition for skip_black
2012-10-10, by Andreas Lochbihler
merged
2012-10-10, by wenzelm
merged
2012-10-10, by hoelzl
infprod generator works also with empty index set
2012-10-10, by hoelzl
add finite entropy
2012-10-10, by hoelzl
continuous version of mutual_information_eq_entropy_conditional_entropy
2012-10-10, by hoelzl
add induction for real Borel measurable functions
2012-10-10, by hoelzl
induction prove for positive_integral_fst
2012-10-10, by hoelzl
strong nonnegativ (instead of ae nn) for induction rule
2012-10-10, by hoelzl
induction prove for positive_integral_density
2012-10-10, by hoelzl
add induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
introduce induction rules for simple functions and for Borel measurable functions
2012-10-10, by hoelzl
joint distribution of independent variables
2012-10-10, by hoelzl
indep_vars does not need sigma-sets
2012-10-10, by hoelzl
simplified definitions
2012-10-10, by hoelzl
remove unnecessary assumption from conditional_entropy_eq
2012-10-10, by hoelzl
alternative definition of conditional entropy
2012-10-10, by hoelzl
remove unneeded assumption from conditional_entropy_generic_eq
2012-10-10, by hoelzl
add induction rule for intersection-stable sigma-sets
2012-10-10, by hoelzl
show and use distributed_swap and distributed_jointI
2012-10-10, by hoelzl
rule to show that conditional mutual information is non-negative in the continuous case
2012-10-10, by hoelzl
continuous version of entropy_le
2012-10-10, by hoelzl
simplified entropy_uniform
2012-10-10, by hoelzl
remove incseq assumption from measure_eqI_generator_eq
2012-10-10, by hoelzl
generalize from prob_space to finite_measure
2012-10-10, by hoelzl
add measurable_compose
2012-10-10, by hoelzl
simplified assumptions for kolmogorov_0_1_law
2012-10-10, by hoelzl
merge should operate on pairs
2012-10-10, by hoelzl
remove incseq assumption from sigma_prod_algebra_sigma_eq
2012-10-10, by hoelzl
sigma_finite_iff_density_finite does not require a positive density function
2012-10-10, by hoelzl
tuned Lebesgue measure proofs
2012-10-10, by hoelzl
tuned product measurability
2012-10-10, by hoelzl
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
2012-10-10, by hoelzl
use continuity to show Borel-measurability
2012-10-10, by hoelzl
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
2012-10-10, by hoelzl
rename terminal_events to tail_event
2012-10-10, by hoelzl
merged
2012-10-10, by Andreas Lochbihler
efficient construction of red black trees from sorted associative lists
2012-10-10, by Andreas Lochbihler
more explicit code equations
2012-10-10, by haftmann
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
2012-10-10, by bulwahn
special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)
2012-10-10, by bulwahn
test case for set_comprehension_pointfree simproc succeeds now
2012-10-10, by bulwahn
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
2012-10-10, by bulwahn
moving simproc from Finite_Set to more appropriate Product_Type theory
2012-10-10, by bulwahn
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
2012-10-10, by bulwahn
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
2012-10-10, by bulwahn
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
2012-10-10, by bulwahn
more consistent error messages on malformed code equations
2012-10-10, by haftmann
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
2012-10-09, by huffman
use Set.filter instead of Finite_Set.filter, which is removed then
2012-10-09, by kuncar
rename Set.project to Set.filter - more appropriate name
2012-10-09, by kuncar
added some ad-hoc namespace prefixes to avoid duplicate facts;
2012-10-10, by wenzelm
avoid duplicate facts;
2012-10-10, by wenzelm
more explicit namespace prefix for 'statespace' -- duplicate facts;
2012-10-10, by wenzelm
eliminated spurious fact duplicates;
2012-10-10, by wenzelm
modernized dynamic "rules" -- avoid rebinding of static facts;
2012-10-10, by wenzelm
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
2012-10-09, by wenzelm
clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
2012-10-09, by wenzelm
more explicit flags for facts table;
2012-10-09, by wenzelm
minor tuning;
2012-10-09, by wenzelm
more conventional Double constants;
2012-10-09, by wenzelm
tuned source structure;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
tuned;
2012-10-09, by wenzelm
merged
2012-10-09, by wenzelm
added type annotations to generated Isar proofs -- code by Steffen Smolka
2012-10-09, by blanchet
consolidated names of theorems on composition;
2012-10-08, by haftmann
corrected NEWS
2012-10-08, by haftmann
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
2012-10-08, by wenzelm
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
2012-10-08, by wenzelm
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
2012-10-08, by wenzelm
tuned;
2012-10-08, by wenzelm
prefer synchronous Mutator_Event.Bus on Swing_Thread;
2012-10-08, by wenzelm
more direct tooltip content;
2012-10-08, by wenzelm
tuned;
2012-10-08, by wenzelm
use Pretty_Tooltip for Graphview_Panel;
2012-10-08, by wenzelm
more basic tooltips;
2012-10-08, by wenzelm
close tooltips more thoroughly;
2012-10-07, by wenzelm
make buttons closer to original mouse position;
2012-10-07, by wenzelm
detach tooltip as dockable window;
2012-10-07, by wenzelm
explicit close button;
2012-10-07, by wenzelm
congruence rule for Finite_Set.fold
2012-10-06, by haftmann
alternative simplification of ^^ to the righthand side;
2012-10-06, by haftmann
eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;
2012-10-05, by wenzelm
merged
2012-10-05, by wenzelm
newer versions of Z3 call it "Bool" not "bool"
2012-10-05, by blanchet
simplified type of msetprod;
2012-10-04, by haftmann
tuned proof
2012-10-04, by haftmann
default simp rule for image under identity
2012-10-04, by haftmann
dropped duplicate facts; tuned syntax
2012-10-04, by haftmann
more facts on setsum and setprod
2012-10-04, by haftmann
made SML/NJ happier
2012-10-04, by traytel
do not expose details of internal data structures for composition of BNFs
2012-10-04, by traytel
further support for nested tooltips;
2012-10-05, by wenzelm
tuned proofs;
2012-10-05, by wenzelm
refer to parent frame -- relevant for floating dockables in particular;
2012-10-05, by wenzelm
tuned window position to fit on screen;
2012-10-05, by wenzelm
tuned window position;
2012-10-05, by wenzelm
determine window size from content;
2012-10-05, by wenzelm
tuned color and font size;
2012-10-05, by wenzelm
close tooltip window on escape;
2012-10-05, by wenzelm
proper message markup for output;
2012-10-05, by wenzelm
some re-ordering of initialization to ensure proper formatting;
2012-10-04, by wenzelm
separate module Pretty_Tooltip;
2012-10-04, by wenzelm
refined rich tooltip options;
2012-10-04, by wenzelm
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
2012-10-04, by wenzelm
some documentation of show_markup;
2012-10-04, by wenzelm
tuned proofs;
2012-10-04, by wenzelm
option to bypass potentially slow text overview;
2012-10-04, by wenzelm
tuned signature;
2012-10-04, by wenzelm
clarified platform dependency;
2012-10-04, by wenzelm
updated crontab and afp-poly settings
2012-10-04, by Gerwin Klein
thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-10-03, by blanchet
made code more conform to rest of BNF package
2012-10-03, by blanchet
more error positions;
2012-10-03, by wenzelm
more explicit show_type_constraint, show_sort_constraint;
2012-10-03, by wenzelm
recovered print translation after 'a => bool to 'a set change;
2012-10-03, by wenzelm
tuned;
2012-10-03, by wenzelm
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-10-03, by wenzelm
printed "_ofsort" is subject to show_markup as well;
2012-10-03, by wenzelm
allow position constraints to coexist with 0 or 1 sort constraints;
2012-10-03, by wenzelm
made tactic more robust (less usage of stac)
2012-10-02, by traytel
continued changing type of corec type
2012-10-02, by blanchet
removed dead params and dead code
2012-10-02, by blanchet
changed type of corecursor for the nested recursion case
2012-10-02, by blanchet
made (co)rec tactic more robust when the simplifier succeeds early
2012-10-02, by blanchet
tuned;
2012-10-01, by wenzelm
removed unused module Blob;
2012-10-01, by wenzelm
more direct message header: eliminated historic encoding via single letter;
2012-10-01, by wenzelm
tuned whitespace;
2012-10-01, by wenzelm
tuned proofs;
2012-10-01, by wenzelm
report sort assignment of visible type variables;
2012-10-01, by wenzelm
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
2012-10-01, by wenzelm
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01, by blanchet
tweaked corecursor/coiterator tactic
2012-10-01, by blanchet
changed the type of the recursor for nested recursion
2012-10-01, by blanchet
fixed quick-and-dirty mode
2012-09-30, by blanchet
tuning
2012-09-30, by blanchet
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
2012-09-30, by traytel
got rid of subst_tac alias
2012-09-30, by traytel
tuned tactic
2012-09-30, by traytel
tuned proofs;
2012-09-29, by wenzelm
tuned proofs;
2012-09-29, by wenzelm
proper handling of constraints stemming from idtyp_ast_tr';
2012-09-29, by wenzelm
enable show_markup by default (approx. double output size);
2012-09-29, by wenzelm
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-29, by wenzelm
explicit show_types takes preferenced over show_markup;
2012-09-29, by wenzelm
ignore wrapped markup elements in Proof General;
2012-09-29, by wenzelm
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
2012-09-29, by wenzelm
treat wrapped markup elements as raw markup delimiters;
2012-09-29, by wenzelm
tuned signature;
2012-09-29, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned;
2012-09-28, by wenzelm
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28, by wenzelm
merged
2012-09-28, by wenzelm
eliminated dead code;
2012-09-28, by wenzelm
smarter handling of tracing messages;
2012-09-28, by wenzelm
display number of tracing messages;
2012-09-28, by wenzelm
tuned signature;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
simplified simpset
2012-09-28, by blanchet
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28, by blanchet
tuned tactic
2012-09-28, by traytel
updated keywords using proper "isabelle update_keywords";
2012-09-28, by wenzelm
tuned tactic
2012-09-28, by traytel
tuned tactic
2012-09-28, by traytel
merge
2012-09-28, by blanchet
renamed ML file in preparation for next step
2012-09-28, by blanchet
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28, by blanchet
modernized example, exploiting "rep_compat" option
2012-09-28, by blanchet
compatibility option to use "rep_datatype"
2012-09-28, by blanchet
tuned message
2012-09-28, by blanchet
modernized example
2012-09-28, by blanchet
tuned tactics
2012-09-28, by traytel
second usage of const_typ
2012-09-28, by nipkow
new antiquotation const_typ
2012-09-28, by nipkow
tuned printing of _ in latex
2012-09-28, by nipkow
mk_readable_rsp_thm_eq is more robust now
2012-09-27, by kuncar
new get function for non-symmetric relator_eq & tuned
2012-09-27, by kuncar
merged
2012-09-27, by wenzelm
tuned tactic; got rid of substs_tac alias
2012-09-27, by traytel
use a nicer scheme to indexify names
2012-09-27, by blanchet
tuned tactic
2012-09-27, by traytel
type of the bound of a BNF depends at most on dead type variables
2012-09-27, by traytel
repaired signature
2012-09-27, by blanchet
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-27, by blanchet
modernized examples
2012-09-27, by blanchet
merged
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
operations to turn markup into XML;
2012-09-27, by wenzelm
removed obsolete org.w3c.dom operations;
2012-09-27, by wenzelm
eliminated obsolete HTML/CSS functionality;
2012-09-27, by wenzelm
removed obsolete Output1 dockable;
2012-09-27, by wenzelm
physical File.eq in conformance to Isabelle/ML;
2012-09-27, by wenzelm
tuned proofs;
2012-09-27, by wenzelm
tuned;
2012-09-27, by wenzelm
updated to consolidated SortedMap in scala-2.9.x;
2012-09-27, by wenzelm
partly ported "TreeFI" example to new syntax
2012-09-27, by blanchet
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-27, by blanchet
tuned
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
merge
2012-09-27, by blanchet
modernized examples;
2012-09-27, by blanchet
some support for jEdit warmstart;
2012-09-26, by wenzelm
discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-09-26, by wenzelm
tuned message;
2012-09-26, by wenzelm
merged
2012-09-26, by wenzelm
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-26, by blanchet
got rid of other instance of shaky "Thm.generalize"
2012-09-26, by blanchet
tweaked theorem names (in particular, dropped s's)
2012-09-26, by blanchet
get rid of shaky "Thm.generalize"
2012-09-26, by blanchet
fixed "rels" + split them into injectivity and distinctness
2012-09-26, by blanchet
generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26, by blanchet
added coinduction tactic
2012-09-26, by blanchet
generalized tactic a bit
2012-09-26, by blanchet
export "dtor_map_coinduct" theorems, since they're used in one example
2012-09-26, by blanchet
name tuning
2012-09-26, by blanchet
parameterized "subst_tac"
2012-09-26, by blanchet
generate high-level "maps", "sets", and "rels" properties
2012-09-26, by blanchet
use singular since there is always only one theorem
2012-09-26, by blanchet
nicer type var names
2012-09-26, by blanchet
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
2012-09-26, by blanchet
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
2012-09-26, by blanchet
leave out some internal theorems unless "bnf_note_all" is set
2012-09-26, by blanchet
tuned
2012-09-26, by nipkow
added counterexamples
2012-09-26, by nipkow
tuned
2012-09-26, by nipkow
tuned
2012-09-25, by nipkow
more uniform graphview terminology;
2012-09-26, by wenzelm
proper Symbol.decode -- especially relevant for Proof General;
2012-09-26, by wenzelm
suppress empty tooltips;
2012-09-26, by wenzelm
obsolete;
2012-09-26, by wenzelm
updated keywords;
2012-09-26, by wenzelm
more uniform graphview terminology;
2012-09-26, by wenzelm
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-09-26, by wenzelm
proper install_fonts;
2012-09-26, by wenzelm
proper jvmpath for Windows;
2012-09-25, by wenzelm
basic integration of graphview into document model;
2012-09-25, by wenzelm
ML support for generic graph display, with browser and graphview backends (via print modes);
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
more complete build;
2012-09-25, by wenzelm
proper error message;
2012-09-25, by wenzelm
separate module Graph_Display;
2012-09-25, by wenzelm
added graph encode/decode operations;
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
minimal component and build setup for graphview;
2012-09-24, by wenzelm
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
2012-09-24, by Markus Kaiser
made smlnj even happier
2012-09-24, by haftmann
tuned proofs;
2012-09-24, by wenzelm
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
2012-09-24, by wenzelm
updated checksum, which appears to have changed accidentally;
2012-09-24, by wenzelm
updated to exec_process-1.0.2;
2012-09-24, by wenzelm
search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);
2012-09-24, by wenzelm
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
2012-09-24, by wenzelm
Mirabelle appears to work better in single-threaded mode;
2012-09-24, by wenzelm
generalized types
2012-09-24, by nipkow
tuned termination proof
2012-09-24, by nipkow
adapted examples to new names
2012-09-23, by blanchet
renamed coinduction principles to have "dtor" in the name
2012-09-23, by blanchet
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed "map_simps" to "{c,d}tor_maps"
2012-09-23, by blanchet
took out accidentally submitted "tracing" calls
2012-09-23, by blanchet
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
2012-09-23, by blanchet
simplified fact policies
2012-09-23, by blanchet
generate "rel_as_srel" and "rel_flip" properties
2012-09-23, by blanchet
started work on generation of "rel" theorems
2012-09-23, by blanchet
make smlnj happy
2012-09-23, by haftmann
more strict typscheme_equiv check: must fix variables of more specific type;
2012-09-22, by haftmann
cache should not contain material from descendant theory
2012-09-22, by haftmann
some PIDE NEWS from this summer;
2012-09-22, by wenzelm
tuned whitespace;
2012-09-22, by wenzelm
tuned;
2012-09-22, by wenzelm
tuned proofs;
2012-09-22, by wenzelm
report proper binding positions only -- avoid swamping document model with unspecific information;
2012-09-22, by wenzelm
accumulate under exec_id as well;
2012-09-22, by wenzelm
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
2012-09-22, by wenzelm
misc tuning;
2012-09-22, by wenzelm
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
2012-09-22, by wenzelm
tuned signature;
2012-09-22, by wenzelm
tuned proofs;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
tighten margin for TextArea instead of Lobo;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
renamed LFP low-level rel property to have ctor not dtor in its name
2012-09-21, by blanchet
changed base session for "HOL-BNF" for faster building in the typical case
2012-09-21, by blanchet
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
2012-09-21, by blanchet
fixed a few names that escaped the renaming
2012-09-21, by blanchet
tuned whitespace
2012-09-21, by blanchet
merged
2012-09-21, by wenzelm
clean up lemmas used for composition
2012-09-21, by blanchet
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
2012-09-21, by blanchet
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-21, by blanchet
renamed top-level theory from "Codatatype" to "BNF"
2012-09-21, by blanchet
adapted examples to renamings
2012-09-21, by blanchet
renamed "pred" to "rel" (relator)
2012-09-21, by blanchet
renamed "rel" to "srel"
2012-09-21, by blanchet
fixed bug introduced by fold/unfold renaming
2012-09-21, by blanchet
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
2012-09-21, by blanchet
simplified code
2012-09-21, by blanchet
tuned a few ML names
2012-09-21, by blanchet
renamed "fld"/"unf" to "ctor"/"dtor"
2012-09-21, by blanchet
tuning
2012-09-21, by blanchet
renamed "upto" coinduction "strong"
2012-09-21, by blanchet
tuned variable names
2012-09-21, by blanchet
tuned names
2012-09-21, by nipkow
more termination proofs
2012-09-21, by nipkow
rel_Gr does not depend on map_wpull
2012-09-21, by traytel
renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
2012-09-21, by wenzelm
more realistic sendback: pick exec_id from message position and text from buffer;
2012-09-21, by wenzelm
some support for hovering and sendback area;
2012-09-21, by wenzelm
merged
2012-09-21, by wenzelm
tuned antiquotations
2012-09-21, by traytel
merged
2012-09-21, by wenzelm
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
2012-09-21, by traytel
conected CS to big-step
2012-09-21, by nipkow
generate "expand" property
2012-09-21, by blanchet
merge
2012-09-20, by blanchet
finished "disc_coiter_iff" etc. generation
2012-09-20, by blanchet
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
2012-09-20, by blanchet
generate coiter_iff and corec_iff theorems
2012-09-20, by blanchet
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
2012-09-20, by Andreas Lochbihler
more efficient code setup
2012-09-20, by Andreas Lochbihler
added "simp"s to coiter/corec theorems + export under "simps" name
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
tuned
2012-09-20, by nipkow
less rendering (cf. 28bd0709443a) -- avoid conflict with static token markup of different keyword kinds;
2012-09-21, by wenzelm
tuned painter;
2012-09-20, by wenzelm
clarified message background;
2012-09-20, by wenzelm
tuned rendering;
2012-09-20, by wenzelm
no caret painting;
2012-09-20, by wenzelm
text_rendering as managed task, with cancellation;
2012-09-20, by wenzelm
more management of Invoke_Scala tasks;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
tuned;
2012-09-20, by wenzelm
removed lpfp and proved least pfp thm
2012-09-20, by nipkow
provide predicator, define relator
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
adapting "More_BNFs" to new relators/predicators
2012-09-20, by blanchet
fixed infinite loop with trivial rel_O_Gr + tuning
2012-09-20, by blanchet
adapted FP code to new relator approach
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
renamed "bnf_fp_util.ML" to "bnf_fp.ML"
2012-09-20, by blanchet
adapted BNF composition to new relator approach
2012-09-20, by blanchet
don't define relators unless necessary
2012-09-20, by blanchet
moved predicator definition before after_qed
2012-09-20, by blanchet
add rel as first-class citizen of BNF
2012-09-20, by blanchet
renamed "rel_def" to "rel_O_Gr"
2012-09-20, by blanchet
renamed "sum_setl" to "setl" and similarly for r
2012-09-20, by blanchet
tuned ID/DEADID setup
2012-09-20, by blanchet
JavaFX is inactive by default;
2012-09-19, by wenzelm
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-19, by wenzelm
universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
2012-09-19, by wenzelm
more direct GUI component;
2012-09-19, by wenzelm
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-19, by wenzelm
made SML/NJ happy;
2012-09-19, by wenzelm
tuned;
2012-09-19, by wenzelm
merged
2012-09-19, by wenzelm
recording elapsed time in mutabelle for more detailed evaluation
2012-09-19, by bulwahn
Added missing predicators (for multisets and countable sets)
2012-09-18, by popescua
added top-level theory for Cardinals
2012-09-18, by popescua
group "simps" together
2012-09-18, by blanchet
register induct attributes
2012-09-18, by blanchet
further tuned simpset
2012-09-18, by blanchet
bnf_note_all mode for "pre_"-BNFs
2012-09-18, by traytel
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
2012-09-18, by traytel
tuned
2012-09-18, by nipkow
beautified names
2012-09-18, by nipkow
proved all upper bounds
2012-09-18, by nipkow
tuned simpset
2012-09-17, by blanchet
cleaner way of dealing with the set functions of sums and products
2012-09-17, by blanchet
handle the general case with more than two levels of nesting when discharging induction prem prems
2012-09-17, by blanchet
clean unfolding of prod and sum sets
2012-09-17, by blanchet
got rid of one "auto" in induction tactic
2012-09-17, by blanchet
cleaned up internal naming scheme for bnfs
2012-09-17, by traytel
more robust GUI component handlers;
2012-09-19, by wenzelm
more rendering;
2012-09-18, by wenzelm
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
2012-09-18, by wenzelm
output is read-only;
2012-09-18, by wenzelm
token marker for extended syntax styles;
2012-09-18, by wenzelm
pass base_snapshot to enable hyperlinks into other nodes;
2012-09-18, by wenzelm
more explicit message markup and rendering;
2012-09-18, by wenzelm
recover order of stacked markup;
2012-09-18, by wenzelm
some actual rich text markup via XML.content_markup;
2012-09-18, by wenzelm
proper separation of output messages;
2012-09-18, by wenzelm
some support for inital command markup;
2012-09-18, by wenzelm
more static rendering state;
2012-09-18, by wenzelm
Pretty_Text_Area is based on Rich_Text_Area;
2012-09-18, by wenzelm
renamed Text_Area_Painter to Rich_Text_Area;
2012-09-17, by wenzelm
tuned signature -- more general Text_Area_Painter operations;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
somewhat more general JEdit_Lib;
2012-09-17, by wenzelm
prefer official polyml-5.5.0;
2012-09-17, by wenzelm
bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;
2012-09-17, by wenzelm
merged
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
updated to polyml-5.5.0;
2012-09-17, by wenzelm
some updates for polyml-5.5.0;
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
2012-09-16, by wenzelm
got rid of ad-hoc lift function
2012-09-16, by nipkow
converted wt into a set, tuned names
2012-09-16, by nipkow
use strip_typeN in bnf_def (instead of repairing strip_type)
2012-09-16, by traytel
removing find_theorems commands that were left in the developments accidently
2012-09-16, by bulwahn
tuning
2012-09-15, by blanchet
tuned code to avoid special case for "fun"
2012-09-15, by blanchet
tuned induction tactic
2012-09-15, by blanchet
tuned error message
2012-09-15, by blanchet
tuning
2012-09-15, by blanchet
typeclass formalising bounded subtraction
2012-09-15, by haftmann
dropped some unused identifiers
2012-09-15, by haftmann
export rel_mono theorem
2012-09-15, by traytel
merged two unfold steps
2012-09-14, by blanchet
took out one rotate_tac
2012-09-14, by blanchet
killed spurious rotate_tac; use auto instead of blast
2012-09-14, by blanchet
moved blast tactic to where it is actually needed
2012-09-14, by blanchet
fixed bug in "mk_map" for the "fun" case
2012-09-14, by blanchet
correct generalization to 3 or more mutually recursive datatypes
2012-09-14, by blanchet
provide more guidance, exploiting our knowledge of the goal
2012-09-14, by blanchet
fixed issue with bound variables in prem prems + tuning
2012-09-14, by blanchet
use right version of "mk_UnIN"
2012-09-14, by blanchet
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14, by blanchet
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14, by blanchet
tuned proofs;
2012-09-14, by wenzelm
merged
2012-09-14, by wenzelm
polished the induction
2012-09-14, by blanchet
put the flat at the right place (to avoid exceptions)
2012-09-14, by blanchet
fixed variable exporting problem
2012-09-14, by blanchet
compile
2012-09-14, by blanchet
added induct tactic
2012-09-14, by blanchet
tuning
2012-09-14, by blanchet
renamed "mk_UnN" to "mk_UnIN"
2012-09-14, by blanchet
merged two commands
2012-09-14, by blanchet
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-14, by blanchet
distinguish between nested and nesting BNFs
2012-09-14, by blanchet
make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14, by blanchet
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-14, by blanchet
no longer react on global_settings (cf. 34ac36642a31);
2012-09-14, by wenzelm
refined output panel: more value-oriented approach to update and caret focus;
2012-09-14, by wenzelm
clarified markup names;
2012-09-14, by wenzelm
more general Document_Model.point_range;
2012-09-14, by wenzelm
more static handling of rendering options;
2012-09-14, by wenzelm
tuned options (again);
2012-09-14, by wenzelm
more scalable option-group;
2012-09-14, by wenzelm
tuned
2012-09-14, by nipkow
merged
2012-09-13, by wenzelm
tuned proofs;
2012-09-13, by wenzelm
remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13, by hoelzl
workaround for HOL-Mirabelle-ex oddities;
2012-09-13, by wenzelm
instructions for quick start in 20min;
2012-09-13, by wenzelm
more liberal init_components: base dir may get created later when resolving missing components;
2012-09-13, by wenzelm
more efficient painting based on cached result;
2012-09-13, by wenzelm
more standard init_components -- particularly important to pick up correct jdk/scala version;
2012-09-13, by wenzelm
tuned
2012-09-13, by nipkow
merged
2012-09-12, by wenzelm
rough and ready induction
2012-09-12, by blanchet
nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
2012-09-12, by blanchet
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12, by wenzelm
eliminated some old material that is unused in the visible universe;
2012-09-12, by wenzelm
tuning
2012-09-12, by blanchet
set up things for (co)induction sugar
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added sumEN_tupled_balanced
2012-09-12, by blanchet
load fonts into JavaFX as well;
2012-09-12, by wenzelm
some support for actual HTML rendering;
2012-09-12, by wenzelm
merged
2012-09-12, by wenzelm
free variable name tuning
2012-09-12, by blanchet
reuse generated names (they look better + slightly more efficient)
2012-09-12, by blanchet
desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12, by blanchet
avoided duplicate lemma
2012-09-12, by blanchet
put an underscore between names, for compatibility with old package (and also because it makes sense)
2012-09-12, by blanchet
got rid of metis calls
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-12, by wenzelm
standardized ML aliases;
2012-09-12, by wenzelm
tuned headers;
2012-09-12, by wenzelm
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-12, by wenzelm
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
2012-09-12, by wenzelm
more robust interrupt handling;
2012-09-12, by wenzelm
some attempts to synchronize ROOT/files and document/build;
2012-09-12, by wenzelm
tuned error;
2012-09-12, by wenzelm
option_pred characterization
2012-09-12, by traytel
true vs. True in pattern matching
2012-09-12, by traytel
reduced theory dependencies
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
moved theorems closer to where they are used
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-12, by blanchet
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
2012-09-12, by blanchet
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning annotations
2012-09-12, by blanchet
tuned antiquotations
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added optional qualifiers for constructors and destructors, similarly to the old package
2012-09-12, by blanchet
adapted example
2012-09-12, by blanchet
added attributes to theorems
2012-09-12, by blanchet
merged
2012-09-11, by wenzelm
support for sort constraints in new (co)data commands
2012-09-11, by blanchet
provide a programmatic interface for FP sugar
2012-09-11, by blanchet
some GUI support for color options;
2012-09-11, by wenzelm
more precise sections;
2012-09-11, by wenzelm
provide color values via options;
2012-09-11, by wenzelm
prefer tuning parameters as public methods (again) -- to allow overriding in applications;
2012-09-11, by wenzelm
updated keywords;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
tuned;
2012-09-11, by wenzelm
more informative tooltip: default value;
2012-09-11, by wenzelm
more options;
2012-09-11, by wenzelm
allow defaults for one datatype to involve the constructor of another one in the mutually recursive case
2012-09-11, by blanchet
added "defaults" option
2012-09-11, by blanchet
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
2012-09-11, by blanchet
spin off "bnf_def_tactics.ML"
2012-09-11, by blanchet
move "bnf_util.ML" to "BNF_Util.thy"
2012-09-11, by blanchet
renamed "BNF_Library" to "BNF_Util"
2012-09-11, by blanchet
generate all sel theorems
2012-09-11, by blanchet
allow default values for selectors in low-level "wrap_data" command
2012-09-11, by blanchet
removed needless "infer_types" call
2012-09-11, by blanchet
added no_dests option
2012-09-11, by blanchet
tuning
2012-09-11, by blanchet
finished splitting sum types for corecursors
2012-09-11, by blanchet
split sum types in corecursor definition
2012-09-11, by blanchet
first step towards splitting corecursor function arguments into (p, g, h) triples
2012-09-11, by blanchet
reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced
2012-09-11, by blanchet
replaced jedit_relative_font_size by jedit_font_scale;
2012-09-11, by wenzelm
need to provide label via some jEdit property;
2012-09-11, by wenzelm
some support to organize options in sections;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
generate "id" rather than (%v. v)
2012-09-11, by blanchet
correctly generate sel_coiter and sel_corec theorems
2012-09-11, by blanchet
generate "sel_coiters" and friends
2012-09-10, by blanchet
sanity check
2012-09-10, by blanchet
implemented and use "mk_sum_casesN_balanced"
2012-09-10, by blanchet
fixed general case of "mk_sumEN_balanced"
2012-09-10, by blanchet
debug
2012-09-10, by blanchet
fixed base case of "mk_sumEN_balanced"
2012-09-10, by blanchet
prevent inconsistent selector types
2012-09-10, by blanchet
minor optimization
2012-09-10, by blanchet
allow same selector name for several constructors
2012-09-10, by blanchet
removed done TODO
2012-09-10, by blanchet
avoid type inference + tuning
2012-09-10, by blanchet
use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-10, by blanchet
busted -- let's use more neutral names
2012-09-10, by blanchet
replacing own dummy value by Haskell's Prelude.undefined
2012-09-10, by bulwahn
prefer global default font over IsabelleText of jEdit TextArea;
2012-09-11, by wenzelm
uniform operation on initial delay;
2012-09-11, by wenzelm
option jedit_load_delay;
2012-09-10, by wenzelm
dynamic evaluation of time (e.g. via options);
2012-09-10, by wenzelm
proper multi-line tooltip;
2012-09-10, by wenzelm
more detailed option tooltip;
2012-09-10, by wenzelm
more systematic JEdit_Options.make_component;
2012-09-10, by wenzelm
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
2012-09-10, by wenzelm
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
simplify "Process" example even further
2012-09-10, by traytel
stabilized generation of parameterized theorem
2012-09-10, by traytel
added snippets
2012-09-10, by nipkow
simplify "Process" example further
2012-09-09, by blanchet
simplify "Process" example
2012-09-09, by blanchet
full name of a type as key in bnf table
2012-09-09, by traytel
fixed bug with one-value codatatype "codata 'a dead_foo = A"
2012-09-09, by blanchet
tuning
2012-09-09, by blanchet
fixed and reenabled "corecs" theorems
2012-09-09, by blanchet
fixed and enabled generation of "coiters" theorems, including the recursive case
2012-09-09, by blanchet
generate "fld_unf_corecs" as well
2012-09-09, by blanchet
reactivated generation of "coiters" theorems
2012-09-09, by blanchet
use map_id, not map_id', to allow better composition
2012-09-09, by blanchet
open typedefs everywhere in the package
2012-09-09, by traytel
open typedef for datatypes
2012-09-09, by traytel
fixed and enabled iterator/recursor theorems
2012-09-08, by blanchet
renamed for consistency
2012-09-08, by blanchet
oops
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
2012-09-08, by blanchet
fixed bug with one-value types with phantom type arguments
2012-09-08, by blanchet
imported patch debugging
2012-09-08, by blanchet
repaired "nofail4" example
2012-09-08, by blanchet
renamed xxxBNF to pre_xxx
2012-09-08, by blanchet
fixed handling of map of "fun"
2012-09-08, by blanchet
comment out code that's not ready
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
construct the right iterator theorem in the recursive case
2012-09-08, by blanchet
some work on coiter tactic
2012-09-08, by blanchet
more sugar on codatatypes
2012-09-08, by blanchet
define corecursors
2012-09-08, by blanchet
define coiterators
2012-09-08, by blanchet
TODO
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
completed iter/rec proofs
2012-09-08, by blanchet
TODOs
2012-09-08, by blanchet
implemented "mk_iter_or_rec_tac"
2012-09-08, by blanchet
generate iter/rec goals
2012-09-08, by blanchet
repaired constant types
2012-09-08, by blanchet
some work towards iterator and recursor properties
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
correctly curry recursor arguments
2012-09-08, by blanchet
added high-level recursor, not yet curried
2012-09-08, by blanchet
merged
2012-09-07, by wenzelm
tuned proofs;
2012-09-07, by wenzelm
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
2012-09-07, by wenzelm
more explicit Delay operations;
2012-09-07, by wenzelm
tuned proofs;
2012-09-07, by wenzelm
clearer names for functions in Quickcheck's narrowing engine
2012-09-07, by bulwahn
merged
2012-09-07, by nipkow
tuned latex
2012-09-07, by nipkow
lattice instances for option type
2012-09-07, by haftmann
combinator Option.these
2012-09-07, by haftmann
adjusted examples
2012-09-07, by nipkow
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
2012-09-06, by huffman
handle type constructors not known to be a BNF using the DEADID BNF
2012-09-06, by traytel
respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-06, by traytel
gracefully handle shadowing case (fourth step of sugar localization)
2012-09-06, by blanchet
careful about constructor types w.r.t. fake context (third step of localization)
2012-09-06, by blanchet
read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
use "add_type" rather than "add_types_global"
2012-09-06, by blanchet
don't throw away the context when hacking the theory (first step to localize the sugar code)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
2012-09-06, by blanchet
construct high-level iterator RHS
2012-09-06, by blanchet
option for discarding build results, enabled in particular for Isabelle_makeall
2012-09-06, by krauss
by default, only generate one discriminator for a two-value datatype
2012-09-05, by blanchet
eliminated potentially confusing terminology of Scala "layer";
2012-09-05, by wenzelm
merged
2012-09-05, by wenzelm
tuned proofs;
2012-09-05, by wenzelm
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-09-05, by wenzelm
honor mixfix specifications
2012-09-05, by blanchet
code indentation
2012-09-05, by blanchet
print timing information
2012-09-05, by blanchet
adapted example
2012-09-05, by blanchet
check type variables on rhs
2012-09-05, by blanchet
proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;
2012-09-05, by wenzelm
added tooltip to reveal jEdit platform file name;
2012-09-05, by wenzelm
commented out slow examples again
2012-09-05, by blanchet
fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors
2012-09-05, by blanchet
fixed "mk_exhaust_tac" for the nth time
2012-09-05, by blanchet
updated README
2012-09-05, by blanchet
ported "Misc_Codata" to new syntax
2012-09-05, by blanchet
ported "Misc_Data" to new syntax
2012-09-05, by blanchet
error message only in case of an error
2012-09-05, by traytel
do not trivialize important internal theorem in quick_and_dirty mode
2012-09-05, by traytel
merged
2012-09-05, by wenzelm
made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)
2012-09-05, by blanchet
tuning (systematic 1-based indices)
2012-09-05, by blanchet
reindented code
2012-09-05, by blanchet
added TODO
2012-09-05, by blanchet
tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
2012-09-05, by blanchet
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
2012-09-05, by blanchet
don't get confused by extraneous premisses
2012-09-05, by blanchet
added a check
2012-09-05, by blanchet
NEWS; CONTRIBUTORS
2012-09-04, by Christian Sternagel
misc tuning;
2012-09-05, by wenzelm
no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);
2012-09-05, by wenzelm
more conservative rechecking of processed constraints in subtyping constraint simplification
2012-09-05, by traytel
added comment for Dmitriy
2012-09-05, by blanchet
fixed bug in type instantiation of case theorem
2012-09-05, by blanchet
use empty binding rather than "*" for default
2012-09-05, by blanchet
tuned
2012-09-05, by nipkow
fixed bugs in one-constructor case
2012-09-05, by blanchet
smoothly handle one-constructor types
2012-09-04, by blanchet
fixed some type issues in sugar "exhaust_tac"
2012-09-04, by blanchet
optionally provide extra dead variables to the FP constructions
2012-09-04, by blanchet
merged
2012-09-04, by wenzelm
added robustness
2012-09-04, by blanchet
added build option -R;
2012-09-04, by wenzelm
implemented "mk_case_tac" -- and got rid of "cheat_tac"
2012-09-04, by blanchet
define "case" constant
2012-09-04, by blanchet
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
2012-09-04, by blanchet
implemented "mk_half_distinct_tac"
2012-09-04, by blanchet
implemented "mk_inject_tac"
2012-09-04, by blanchet
implemented "mk_exhaust_tac"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04, by blanchet
renamed "disc_exclus" theorem to "disc_exclude"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
smarter "*" syntax -- fallback on "_" if "*" is impossible
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
renamed theorem
2012-09-04, by blanchet
tuned TODO comment
2012-09-04, by blanchet
allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-04, by blanchet
removed oddities
2012-09-04, by blanchet
allow "*" to indicate no discriminator
2012-09-04, by blanchet
tuned TODOs
2012-09-04, by blanchet
started work on sugared "(co)data" commands
2012-09-04, by blanchet
export "wrap" function
2012-09-04, by blanchet
eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
2012-09-04, by traytel
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
2012-09-04, by traytel
enable parallel terminal proofs in interaction;
2012-09-04, by wenzelm
misc tuning;
2012-09-03, by wenzelm
merged
2012-09-03, by wenzelm
killed internal output
2012-09-03, by traytel
generate coinductive witnesses for codatatypes
2012-09-03, by traytel
generalized signature
2012-09-03, by traytel
added examples for testing of coinductive witnesses
2012-09-03, by traytel
continue with more robust dummy session after failed startup;
2012-09-03, by wenzelm
prefer old startup dialog scheme (cf. 514bb82514df);
2012-09-03, by wenzelm
more permissive handling of plugin startup failure;
2012-09-03, by wenzelm
bypass slow check for inlined files, where it is not really required;
2012-09-03, by wenzelm
more direct access to all-important chunks for text painting;
2012-09-03, by wenzelm
merged
2012-09-03, by nipkow
added annotations after condition in if and while
2012-09-03, by nipkow
merge, resolving trivial conflict;
2012-09-03, by wenzelm
forgot to add lemmas
2012-08-30, by Christian Sternagel
hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI
2012-08-30, by Christian Sternagel
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30, by Christian Sternagel
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30, by Christian Sternagel
added theory instantiating type class order for list prefixes
2012-08-30, by Christian Sternagel
Main is implicitly imported via Sublist
2012-08-30, by Christian Sternagel
added author
2012-08-30, by Christian Sternagel
List is implicitly imported by Main
2012-08-30, by Christian Sternagel
introduced "sub" as abbreviation for "emb (op =)";
2012-08-29, by Christian Sternagel
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
2012-08-29, by Christian Sternagel
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
2012-08-29, by Christian Sternagel
more lemmas on suffixes and embedding
2012-08-29, by Christian Sternagel
changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
2012-08-29, by Christian Sternagel
added embedding for lists (constant emb)
2012-08-29, by Christian Sternagel
renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=
2012-08-29, by Christian Sternagel
renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix
2012-08-29, by Christian Sternagel
renamed theory List_Prefix into Sublist (since it is not only about prefixes)
2012-08-29, by Christian Sternagel
compile
2012-09-03, by blanchet
rearrange dependencies
2012-09-03, by blanchet
renamed three BNF/(co)datatype-related commands
2012-09-03, by blanchet
tuned boundary cases of command-line;
2012-09-03, by wenzelm
"isabelle logo" produces EPS and PDF format simultaneously;
2012-09-03, by wenzelm
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
2012-09-03, by wenzelm
tuned proofs;
2012-09-03, by wenzelm
some parallel ML;
2012-09-03, by wenzelm
proper classpath on windows;
2012-09-02, by wenzelm
proper classpath for Java FX;
2012-09-02, by wenzelm
basic setup for HTML5 panel;
2012-09-02, by wenzelm
basic support for Java FX;
2012-09-02, by wenzelm
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
2012-09-02, by wenzelm
removed unused material;
2012-09-01, by wenzelm
discontinued complicated/unreliable notion of recent proofs within context;
2012-09-01, by wenzelm
central management of forked goals wrt. transaction id;
2012-09-01, by wenzelm
merged
2012-08-31, by wenzelm
always register proofs, even for empty binding;
2012-08-31, by wenzelm
tuned signature;
2012-08-31, by wenzelm
made parser a bit more flexible
2012-08-31, by blanchet
tuning
2012-08-31, by blanchet
pad the selectors' list with default names
2012-08-31, by blanchet
generate default names for selectors
2012-08-31, by blanchet
renamed "disc_disjoint" property "disj_exclus"
2012-08-31, by blanchet
optimized "mk_split_tac" + use "notes"
2012-08-31, by blanchet
optimized "mk_case_disc_tac" further
2012-08-31, by blanchet
optimized "mk_case_disc_tac"
2012-08-31, by blanchet
tuning
2012-08-31, by blanchet
rationalized data structure for distinctness theorems
2012-08-31, by blanchet
optimized "case_cong" proof
2012-08-31, by blanchet
allow default names for selectors via wildcard (_) + fix wrong index (k)
2012-08-31, by blanchet
minor fixes (for compatibility with existing datatype package)
2012-08-31, by blanchet
generate "split_asm" property
2012-08-31, by blanchet
generate "split" property
2012-08-31, by blanchet
more precise register_proofs for local goals;
2012-08-31, by wenzelm
more informative error message from failed goal forks (violating old-style TTY protocol!);
2012-08-31, by wenzelm
avoid empty tooltips;
2012-08-31, by wenzelm
clarified command status (again);
2012-08-31, by wenzelm
recovered ScrollPane from d899be1cfe6d;
2012-08-31, by wenzelm
more markup for failed goal forks, reusing "bad";
2012-08-31, by wenzelm
further refinement of command status, to accomodate forked proofs;
2012-08-31, by wenzelm
merged;
2012-08-30, by wenzelm
make parallel list indexing possible for inject theorems
2012-08-30, by blanchet
generate "weak_case_cong" property
2012-08-30, by blanchet
generate "case_cong" property
2012-08-30, by blanchet
generate "case_disc" property
2012-08-30, by blanchet
generate "ctr_sels" theorems
2012-08-30, by blanchet
generate "disc_exhaust" property
2012-08-30, by blanchet
generate "disc_distinct" theorems
2012-08-30, by blanchet
added discriminator theorems
2012-08-30, by blanchet
adjust example
2012-08-30, by blanchet
more work on sugar
2012-08-30, by blanchet
updated Java-related error message
2012-08-30, by blanchet
changed order of arguments to "bnf_sugar"
2012-08-30, by blanchet
define selectors and discriminators
2012-08-30, by blanchet
tuning
2012-08-30, by blanchet
more work on BNF sugar -- up to derivation of nchotomy
2012-08-30, by blanchet
more work on BNF sugar
2012-08-30, by blanchet
renamed ML function for consistency
2012-08-30, by blanchet
started work on datatype sugar
2012-08-30, by blanchet
killed obsolete "bnf_of_typ" command
2012-08-30, by blanchet
removed dead code
2012-08-30, by blanchet
have "bnf_of_typ" command seal the BNF
2012-08-30, by blanchet
register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30, by wenzelm
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30, by wenzelm
some support for registering forked proofs within Proof.state, using its bottom context;
2012-08-30, by wenzelm
tuned signature;
2012-08-30, by wenzelm
refined status of forked goals;
2012-08-30, by wenzelm
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
2012-08-30, by wenzelm
tuned message;
2012-08-29, by wenzelm
discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;
2012-08-29, by wenzelm
approximative build of pdf documents in 1 pass instead of 3;
2012-08-29, by wenzelm
more formal isabelle makedist from repository;
2012-08-29, by wenzelm
removed remains of generated material, which tends to rot;
2012-08-29, by wenzelm
one more round to ensure that base images are already there, without producing document output themselves;
2012-08-29, by wenzelm
more robust document setup;
2012-08-29, by wenzelm
provide polyml-5.4.1 as regular component;
2012-08-29, by wenzelm
clarified handling of raw output messages;
2012-08-29, by wenzelm
no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;
2012-08-29, by wenzelm
command 'use' is legacy;
2012-08-29, by wenzelm
clarified separated_chunks vs. space_explode;
2012-08-29, by wenzelm
more precise indentation;
2012-08-29, by wenzelm
modernized specifications;
2012-08-29, by wenzelm
tuned signature;
2012-08-29, by wenzelm
renamed Position.str_of to Position.here;
2012-08-29, by wenzelm
init components from local clone that is used to produce the test distribition, which itself lacks Admin;
2012-08-29, by wenzelm
discontinued centralistic changelog;
2012-08-28, by wenzelm
discontinued odd copy of eps logos (cf. 8fc3828fdc8a);
2012-08-28, by wenzelm
prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;
2012-08-28, by wenzelm
removed odd left-over file;
2012-08-28, by wenzelm
update on "isabelle build" and "isabelle build_doc";
2012-08-28, by wenzelm
renamed doc-src to src/Doc;
2012-08-28, by wenzelm
do not hardwire document output options -- to be provided by the user;
2012-08-28, by wenzelm
more permanent update of keywords (cf. 3517d6f50b12);
2012-08-28, by wenzelm
merged
2012-08-28, by wenzelm
updated keywords
2012-08-28, by blanchet
fixed import paths in examples
2012-08-28, by blanchet
fixed import paths
2012-08-28, by blanchet
tuning
2012-08-28, by blanchet
updated NEWS and CONTRIBUTORS
2012-08-28, by blanchet
documentation cleanup
2012-08-28, by blanchet
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
2012-08-28, by blanchet
Typo fixed.
2012-08-28, by webertj
updated .hgignore to reflect to (almost) clean result of build_doc;
2012-08-28, by wenzelm
more formal build_doc tool (Admin only);
2012-08-28, by wenzelm
prepare document more uniformly;
2012-08-28, by wenzelm
prefer \input which actually checks file existence;
2012-08-28, by wenzelm
tuned;
2012-08-28, by wenzelm
prefer (old) isa-index as provided here, to get exactly the same index layout as in Isabelle2012;
2012-08-28, by wenzelm
removed old stuff;
2012-08-28, by wenzelm
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
2012-08-28, by wenzelm
removed old stuff;
2012-08-28, by wenzelm
removed historic manual;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
updated IsarRef/document/style.sty;
2012-08-28, by wenzelm
missing file;
2012-08-28, by wenzelm
removed junk;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;
2012-08-28, by wenzelm
prefer doc-src/pdfsetup.sty;
2012-08-28, by wenzelm
more official way to set margin;
2012-08-27, by wenzelm
avoid clash with generated Adaptation.tex on case-insensible file-systems;
2012-08-27, by wenzelm
missing file;
2012-08-27, by wenzelm
deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more portable perl invocation;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
clarified "isabelle logo";
2012-08-27, by wenzelm
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
2012-08-27, by wenzelm
less ambitious test -- terminate more quickly;
2012-08-27, by wenzelm
tuned;
2012-08-27, by wenzelm
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
2012-08-19, by wenzelm
test with many add-ons;
2012-08-27, by wenzelm
updated Theory.begin_theory;
2012-08-26, by wenzelm
entity markup for theory Pure, to enable hyperlinks etc.;
2012-08-26, by wenzelm
more accurate defining position of theory;
2012-08-26, by wenzelm
theory def/ref position reports, which enable hyperlinks etc.;
2012-08-26, by wenzelm
fixed theory dependency
2012-08-26, by nipkow
more convenient switching of buffers;
2012-08-24, by wenzelm
report source path and let front-end resolve implicit master location (e.g. URL);
2012-08-24, by wenzelm
prefer jEdit file name representation (potentially via VFS);
2012-08-24, by wenzelm
more precise counting of line/column;
2012-08-24, by wenzelm
support for direct hyperlinks, without the Hyperlinks plugin;
2012-08-24, by wenzelm
tuned signature;
2012-08-24, by wenzelm
some markup for inlined files;
2012-08-24, by wenzelm
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-24, by wenzelm
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
2012-08-24, by wenzelm
clarified syntax boundary cases and errors;
2012-08-24, by wenzelm
simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;
2012-08-23, by wenzelm
eliminated obsolete byte_reader -- theory headers + body files are parsed in full;
2012-08-23, by wenzelm
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
2012-08-23, by wenzelm
improved errors of parser combinators;
2012-08-23, by wenzelm
tuned messages: end-of-input rarely means physical end-of-file from the past;
2012-08-23, by wenzelm
merged
2012-08-23, by wenzelm
remove Hoare dependency from Fold.thy
2012-08-23, by Gerwin Klein
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
2012-08-23, by wenzelm
turned 'boogie_open' into thy_load command, without any declarations of 'uses';
2012-08-23, by wenzelm
tuned signature;
2012-08-23, by wenzelm
clarified type Token.file;
2012-08-23, by wenzelm
expand all files uniformly;
2012-08-23, by wenzelm
added build option -l (list files);
2012-08-23, by wenzelm
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-08-23, by wenzelm
more basic file dependencies -- no load command here;
2012-08-23, by wenzelm
tuned signature (again, cf. ff9cd47be39b);
2012-08-23, by wenzelm
updated Thy_Load.check_thy;
2012-08-23, by wenzelm
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-23, by wenzelm
tuned signature;
2012-08-23, by wenzelm
simplified Thy_Load.provide: do not store full path;
2012-08-23, by wenzelm
prefer ML_file over old uses;
2012-08-22, by wenzelm
merged
2012-08-22, by wenzelm
abstracted lemmas
2012-08-21, by nipkow
prefer ML_file over old uses;
2012-08-22, by wenzelm
prefer ML_file over old uses;
2012-08-22, by wenzelm
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
2012-08-22, by wenzelm
add keywords of this node as well (e.g. relevant for Pure.thy);
2012-08-22, by wenzelm
tuned;
2012-08-22, by wenzelm
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
2012-08-22, by wenzelm
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
2012-08-22, by wenzelm
find files via load commands within theory text;
2012-08-22, by wenzelm
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
2012-08-22, by wenzelm
pass syntax through check_thy;
2012-08-22, by wenzelm
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
2012-08-22, by wenzelm
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22, by wenzelm
tuned;
2012-08-22, by wenzelm
clarified bootstrapping of Pure;
2012-08-22, by wenzelm
tuned errors;
2012-08-22, by wenzelm
prefer File.full_path in accordance to check_file;
2012-08-21, by wenzelm
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
2012-08-21, by wenzelm
updated Thy_Load.check_thy;
2012-08-21, by wenzelm
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
2012-08-21, by wenzelm
more direct cumulation of (sparse) keywords;
2012-08-21, by wenzelm
some support for thy_load_commands;
2012-08-21, by wenzelm
tuned signature;
2012-08-21, by wenzelm
clarified initialization of Thy_Load, Thy_Info, Session;
2012-08-21, by wenzelm
tuned;
2012-08-21, by wenzelm
more robust cleaning of "% tag" and "-- cmt";
2012-08-20, by wenzelm
some support for inlining file content into outer syntax token language;
2012-08-20, by wenzelm
tuned comment;
2012-08-20, by wenzelm
tuned;
2012-08-20, by wenzelm
added keyword kind "thy_load" (with optional list of file extensions);
2012-08-20, by wenzelm
updated generated files;
2012-08-20, by wenzelm
more strict syntax, according to manual;
2012-08-20, by wenzelm
abstracted lemma
2012-08-20, by nipkow
retain unknown options within preferences;
2012-08-19, by wenzelm
more comprehensible platform family name;
2012-08-19, by wenzelm
tuned message;
2012-08-19, by wenzelm
fewer components, more roots;
2012-08-19, by wenzelm
actually remove makeall (cf. 292b97e17fb7);
2012-08-19, by wenzelm
tuned;
2012-08-17, by wenzelm
Backed out changeset ec82c33c75f8;
2012-08-17, by wenzelm
Typo fixed.
2012-08-17, by webertj
merged
2012-08-17, by wenzelm
merged
2012-08-17, by nipkow
fixed lemmas
2012-08-17, by nipkow
abstracted lemmas
2012-08-16, by nipkow
updated to new init_components, hoping that mira can digest that;
2012-08-17, by wenzelm
some explanations on component categories;
2012-08-17, by wenzelm
specific cygwin components;
2012-08-17, by wenzelm
obsolete;
2012-08-17, by wenzelm
some explanations on isabelle components;
2012-08-17, by wenzelm
some grouping of components;
2012-08-17, by wenzelm
renamed components to components_old, to make room for some directory of the same name;
2012-08-17, by wenzelm
minor robustification;
2012-08-17, by wenzelm
added "isabelle components" tool;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
direct support for component forests via init_components;
2012-08-17, by wenzelm
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
updated component repository;
2012-08-17, by wenzelm
updates on 32 bit vs. 64 bit platforms;
2012-08-17, by wenzelm
updated to jedit_build-20120813, pointing to another contrib directory as a change;
2012-08-17, by wenzelm
merged
2012-08-16, by wenzelm
tuned proofs;
2012-08-16, by wenzelm
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
2012-08-16, by blanchet
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
2012-08-16, by haftmann
more robust multi-platform support;
2012-08-16, by wenzelm
updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
2012-08-16, by wenzelm
support for jdk-7u6 component;
2012-08-16, by wenzelm
Clarification: free variables allowed in interpreted locale instances.
2012-08-15, by ballarin
merged
2012-08-15, by nipkow
fixed proof
2012-08-15, by nipkow
abstracted lemmas
2012-08-15, by nipkow
Backed out changeset 6cf7a9d8bbaf
2012-08-15, by nipkow
abstracted lemmas
2012-08-15, by nipkow
merged
2012-08-15, by webertj
Turned into Admin tool download_components.
2012-08-15, by webertj
tuned;
2012-08-15, by wenzelm
tuned;
2012-08-15, by wenzelm
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
2012-08-15, by wenzelm
tuned;
2012-08-15, by wenzelm
fixed handling of "int" in the wake of its port to the quotient package
2012-08-15, by blanchet
removed dead code
2012-08-15, by blanchet
merged
2012-08-15, by webertj
Added various options, notably -c to download components listed in Admin/components. Also, curl instead of wget.
2012-08-15, by webertj
ignore some administrative files on newer Mercurial versions as well;
2012-08-14, by wenzelm
some support for persistent user preferences;
2012-08-14, by wenzelm
merged
2012-08-14, by wenzelm
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
2012-08-14, by wenzelm
more direct interpretation of document_variants for build (unchanged for usedir);
2012-08-14, by wenzelm
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
2012-08-14, by blanchet
fixed then-else confusion
2012-08-14, by blanchet
tweak Vampire setup in the light of new evaluation
2012-08-14, by blanchet
improved set of reconstructor methods
2012-08-14, by blanchet
warn users about unused "using" facts
2012-08-14, by blanchet
be less aggressive at kicking out chained facts
2012-08-14, by blanchet
recognize bus errors as crash
2012-08-14, by blanchet
consider removing chained facts last, so that they're more likely to be kept
2012-08-14, by blanchet
clarified format of etc/options: only declarations, not re-definitions;
2012-08-14, by wenzelm
check_errors for cumulative session content;
2012-08-14, by wenzelm
even more defensive path expansion (see also 8d381fdef898);
2012-08-14, by wenzelm
support for 'typ' with explicit sort constraint;
2012-08-14, by wenzelm
added jedit option -d;
2012-08-14, by wenzelm
always retain doc-src (as regular component);
2012-08-14, by wenzelm
merged
2012-08-13, by wenzelm
Calling isabelle with proper (relative) path, no longer relying on $PATH.
2012-08-13, by webertj
fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
2012-08-13, by wenzelm
updated to jedit-4.5.2 (still unchanged);
2012-08-13, by wenzelm
restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself
2012-08-12, by krauss
tuned;
2012-08-12, by wenzelm
fixed mira.py (cf. fd50596bf78b)
2012-08-12, by krauss
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
2012-08-12, by wenzelm
more static antiquotations;
2012-08-12, by wenzelm
always show some timing information, to reduce the need for explicit -v;
2012-08-12, by wenzelm
some information for central Isabelle repository configuration;
2012-08-12, by wenzelm
reduced settings patching
2012-08-12, by krauss
removed obsolete configuration AFP_images
2012-08-12, by krauss
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-08-11, by wenzelm
simplified symbol matching;
2012-08-11, by wenzelm
further clarification of malformed symbols;
2012-08-11, by wenzelm
more liberal scanning of potentially malformed symbols;
2012-08-11, by wenzelm
vacuous execution after first malformed command;
2012-08-11, by wenzelm
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-08-11, by wenzelm
tuned markup;
2012-08-11, by wenzelm
tuned message;
2012-08-11, by wenzelm
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-11, by wenzelm
reports with body text, not just markup;
2012-08-11, by wenzelm
fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end
2012-08-11, by blanchet
special code with lists no longer necessary, use sets
2012-08-11, by nipkow
proper error prefixes;
2012-08-10, by wenzelm
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
2012-08-10, by wenzelm
tuned message;
2012-08-10, by wenzelm
clarified Linear_Set.next/prev: check definedness;
2012-08-10, by wenzelm
merged
2012-08-10, by nipkow
Improved complete lattice formalisation - no more index set.
2012-08-10, by nipkow
merged
2012-08-10, by wenzelm
tuned proofs;
2012-08-10, by wenzelm
sneak message into "bad" markup as property -- to be displayed after YXML parsing;
2012-08-10, by wenzelm
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
2012-08-10, by wenzelm
clarified undefined, unparsed, unfinished command spans;
2012-08-10, by wenzelm
tuned;
2012-08-10, by wenzelm
discontinued mostly unused markup for command spans;
2012-08-10, by wenzelm
more visible markup of malformed input as "bad";
2012-08-10, by wenzelm
tuned proofs
2012-08-10, by blanchet
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
2012-08-09, by wenzelm
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
more direct Linear_Set.reverse, swapping orientation of the graph;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
tuned;
2012-08-09, by wenzelm
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
2012-08-09, by wenzelm
explicit FIXME;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
corrected header
2012-08-08, by haftmann
refined isabelle mkroot;
2012-08-08, by wenzelm
simplified session specifications: names are taken verbatim and current directory is default;
2012-08-08, by wenzelm
added build option -D: include session directory and select its sessions;
2012-08-08, by wenzelm
discontinued obsolete "isabelle makeall";
2012-08-08, by wenzelm
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
2012-07-27, by wenzelm
back to implicit commit via isabelle-process -- save image only once (cf. 181b91e1d1c1);
2012-08-08, by wenzelm
proper axiomatization of "mem" -- do not leave it formally unspecified;
2012-08-08, by wenzelm
simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
2012-08-08, by wenzelm
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
2012-08-08, by wenzelm
obsolete;
2012-08-08, by wenzelm
eliminated obsolete ISABELLE_USEDIR_OPTIONS;
2012-08-08, by wenzelm
updated ML settings;
2012-08-08, by wenzelm
add legacy target for HOL-Probability, needed by AFP/Markov_Models
2012-08-08, by hoelzl
proper isabelle update_keywords tool;
2012-08-08, by wenzelm
configure Admin as component, with its own lib/Tools;
2012-08-08, by wenzelm
SOMEthing went utterly wrong in 5b51ccdc8623;
2012-08-08, by wenzelm
more legacy targets;
2012-08-08, by wenzelm
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
2012-08-07, by wenzelm
tuned;
2012-08-07, by wenzelm
proper quoting
2012-08-07, by blanchet
merged
2012-08-07, by wenzelm
more structural parsing for minor modes;
2012-08-07, by wenzelm
clarified Sidekick configuration, including minor modes;
2012-08-07, by wenzelm
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-08-07, by blanchet
specify full path to clausifier
2012-08-07, by blanchet
documentation
2012-08-07, by blanchet
more token markers, based on actual outer syntax;
2012-08-07, by wenzelm
simplified process startup phases: INIT suffices for is_ready;
2012-08-07, by wenzelm
need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
2012-08-07, by wenzelm
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-07, by wenzelm
prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
2012-08-07, by wenzelm
permissive outer syntax wrt. symbol recoding;
2012-08-07, by wenzelm
simplified Document.Node.Header -- internalized errors;
2012-08-07, by wenzelm
tuned signature;
2012-08-07, by wenzelm
tuned signature -- slightly more abstract text representation of prover process;
2012-08-07, by wenzelm
tuned signature -- make Pretty less dependent on Symbol;
2012-08-07, by wenzelm
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
2012-08-07, by boehmes
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
2012-08-07, by boehmes
documentation
2012-08-06, by blanchet
added iProver(-Eq) local
2012-08-06, by blanchet
optimized saving
2012-08-06, by blanchet
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
2012-08-06, by wenzelm
merged
2012-08-06, by wenzelm
switching from Emacs.app to Aquamacs.app
2012-08-06, by paulson
switching from Emacs.app to Aquamacs.app
2012-08-06, by paulson
modify group_cancel simprocs so that they can cancel multiple terms at once
2012-08-06, by huffman
"isabelle options" prints Isabelle system options;
2012-08-06, by wenzelm
removed leftover from 89cc3dfb383b, hoping that mira digests it;
2012-08-06, by wenzelm
discontinued presumably obsolete attempts at doc-src testing (cf. 3b02b0ef8d48, 89cc3dfb383b);
2012-08-06, by wenzelm
more precise imitation of old ROOT.ML files;
2012-08-06, by wenzelm
fixed mira.py (cf. fe611991427a)
2012-08-05, by krauss
corrected session name
2012-08-05, by krauss
removed obsolete mira configurations -- covered by AFP_images
2012-08-05, by krauss
modernized mira configurations, making use of isabelle build
2012-08-05, by krauss
removed mira configurations related to old importer
2012-08-05, by krauss
re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
2012-08-05, by wenzelm
more on isabelle mkroot;
2012-08-05, by wenzelm
added mkroot: prepare session root directory;
2012-08-05, by wenzelm
prefer general Command_Line.tool wrapper (cf. Scala version);
2012-08-05, by wenzelm
simplified Session_Tree;
2012-08-05, by wenzelm
some timeouts, which modify the build order;
2012-08-04, by wenzelm
queue ordering by descending outdegree and timeout;
2012-08-04, by wenzelm
tuned import;
2012-08-04, by wenzelm
clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
2012-08-04, by wenzelm
clarified Session_Entry vs. Session_Info with related parsing operations;
2012-08-04, by wenzelm
simplified class Job;
2012-08-04, by wenzelm
let with_timing report overall number of threads;
2012-08-04, by wenzelm
further robustification of interrupts during build;
2012-08-04, by wenzelm
refined outer syntax;
2012-08-04, by wenzelm
prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);
2012-08-03, by wenzelm
remember ATP flops to avoid repeating them too quickly
2012-08-03, by blanchet
remember which MaSh proofs were found using ATPs
2012-08-03, by blanchet
rule out same "technical" theories for MePo as for MaSh
2012-08-03, by blanchet
don't generate queries for empty dependencies
2012-08-03, by blanchet
crank up max number of dependencies
2012-08-03, by blanchet
never use MaSh in Metis examples, to avoid one dimension of nondeterminism
2012-08-03, by blanchet
merged
2012-08-03, by wenzelm
more informative process exit code;
2012-08-03, by wenzelm
timeout for session build job;
2012-08-03, by wenzelm
static outer syntax based on session specifications;
2012-08-03, by wenzelm
declare trE and tr_induct as default cases and induct rules for type tr
2012-08-03, by huffman
reject path variable nesting explicitly;
2012-08-03, by wenzelm
simplified custom document/build script, instead of old-style document/IsaMakefile;
2012-08-03, by wenzelm
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
2012-08-03, by blanchet
merged
2012-08-02, by wenzelm
don't tag negatively naked variables
2012-08-02, by blanchet
support older versions of Vampire
2012-08-02, by blanchet
document E-MaLeS
2012-08-02, by blanchet
added E-MaLeS to list of provers for testing
2012-08-02, by blanchet
discontinued unused etc/sessions catalog;
2012-08-02, by wenzelm
allow session specifications in arbitrary order;
2012-08-02, by wenzelm
tuned;
2012-08-02, by wenzelm
report commands as formal entities, with def/ref positions;
2012-08-02, by wenzelm
more official command specifications, including source position;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
declare keywords only once;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
more standard bootstrapping of Pure outer syntax;
2012-08-01, by wenzelm
fixed document;
2012-08-01, by wenzelm
store parent heap stamp as well -- needs to be propagated through the build hierarchy;
2012-08-01, by wenzelm
more standard bootstrapping of Pure.thy;
2012-08-01, by wenzelm
more precise guide for bibtex/makeindex -- dummy files should be sufficient;
2012-08-01, by wenzelm
added offline test for skip_proofs;
2012-08-01, by wenzelm
clarified ISABELLE_FULL_TEST;
2012-08-01, by wenzelm
explicit option skip_proofs;
2012-08-01, by wenzelm
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
2012-08-01, by wenzelm
removed junk;
2012-08-01, by wenzelm
no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;
2012-08-01, by wenzelm
more prominent file name;
2012-08-01, by wenzelm
updated isatest settings for isabelle build;
2012-07-31, by wenzelm
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
2012-07-31, by wenzelm
merged
2012-07-31, by wenzelm
print full path;
2012-07-31, by wenzelm
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now
2012-07-31, by kuncar
add testing file for RBT_Set
2012-07-31, by kuncar
implementation of sets by RBT trees for the code generator
2012-07-31, by kuncar
use lifting/transfer formalization of RBT from Lift_RBT
2012-07-31, by kuncar
a couple of additions to RBT formalization to allow us to implement RBT_Set
2012-07-31, by kuncar
more relation operations expressed by Finite_Set.fold
2012-07-31, by kuncar
more set operations expressed by Finite_Set.fold
2012-07-31, by kuncar
moved another larger quickcheck example to Quickcheck_Benchmark
2012-07-26, by bulwahn
HOL-Probability appears to work with smlnj;
2012-07-31, by wenzelm
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
2012-07-31, by wenzelm
made SML/NJ happy;
2012-07-31, by wenzelm
renamed session TLA to HOL-TLA to avoid clash with AFP;
2012-07-31, by wenzelm
clarified directory content operations (similar to ML version);
2012-07-30, by wenzelm
regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);
2012-07-30, by wenzelm
multi-threaded HOL-Tutorial with explicit indication of local options;
2012-07-30, by wenzelm
removed obsolete IsaMakefile + ROOT.ML setup -- doc-src is managed via isabelle build;
2012-07-30, by wenzelm
removed some old material (inactive since 2002/2003);
2012-07-30, by wenzelm
updated isatest to isabelle build, which also includes doc-src sessions;
2012-07-30, by wenzelm
obsolete;
2012-07-30, by wenzelm
makedist -D retains doc-src component with its "doc" sessions (relevant for testing);
2012-07-30, by wenzelm
allow negative int values as well, according to real = int | float;
2012-07-30, by wenzelm
misc tuning;
2012-07-30, by wenzelm
discontinued unused isabelle jedit debugger;
2012-07-30, by wenzelm
more uniform usage of "isabelle tool";
2012-07-30, by wenzelm
less verbosity;
2012-07-30, by wenzelm
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;
2012-07-30, by wenzelm
tuned signature;
2012-07-30, by wenzelm
updated ROOT according to 3defa60a7ae3;
2012-07-30, by wenzelm
merged
2012-07-30, by wenzelm
re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples
2012-07-30, by bulwahn
added build option -c;
2012-07-30, by wenzelm
removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;
2012-07-30, by wenzelm
script for downloading components from central store
2012-07-29, by haftmann
added build option -f;
2012-07-29, by wenzelm
corrected slip
2012-07-28, by haftmann
discontinued $ISABELLE_HOME/build (cf. 500c6eb6c6dc);
2012-07-28, by wenzelm
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
2012-07-28, by wenzelm
added Quickcheck_Benchmark (cf. 1959baa22632);
2012-07-28, by wenzelm
no apparent need for single-threaded execution;
2012-07-28, by wenzelm
discontinued obsolete Isabelle/build script;
2012-07-28, by wenzelm
announce advanced support for Isabelle sessions and build management;
2012-07-28, by wenzelm
some introduction on sessions;
2012-07-28, by wenzelm
tuned messages;
2012-07-28, by wenzelm
tuned;
2012-07-28, by wenzelm
added generated file;
2012-07-28, by wenzelm
some description of main build options;
2012-07-28, by wenzelm
more on "Session ROOT specifications";
2012-07-28, by wenzelm
some description of isabelle build;
2012-07-28, by wenzelm
tuned;
2012-07-28, by wenzelm
isabelle browser is another user interface;
2012-07-28, by wenzelm
renamed isabelle-root minor mode;
2012-07-28, by wenzelm
discontinued special treatment of Proof General;
2012-07-28, by wenzelm
top-down order of user interfaces;
2012-07-28, by wenzelm
misc tuning;
2012-07-28, by wenzelm
move exception handlers outside of let block
2012-07-28, by huffman
tuned message;
2012-07-27, by wenzelm
merged
2012-07-27, by wenzelm
evaluation: allow multiple code modules
2012-07-27, by haftmann
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
merged
2012-07-27, by wenzelm
restored narrowing quickcheck after 6efff142bb54
2012-07-27, by haftmann
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;
2012-07-27, by wenzelm
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
2012-07-27, by huffman
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
2012-07-27, by huffman
give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-07-27, by huffman
tweaks in preparation for type encoding evaluation
2012-07-27, by blanchet
merged
2012-07-27, by wenzelm
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2012-07-27, by huffman
nicer Nitpick subscript output in jEdit
2012-07-27, by blanchet
no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;
2012-07-27, by wenzelm
proper shell variable;
2012-07-27, by wenzelm
actually check return code;
2012-07-27, by wenzelm
include doc-src as component, and thus its sessions defined in ROOT;
2012-07-27, by wenzelm
tuned signature;
2012-07-27, by wenzelm
delete other log file;
2012-07-27, by wenzelm
simplified Path vs. JVM File operations;
2012-07-27, by wenzelm
tuned;
2012-07-27, by wenzelm
tuned messages;
2012-07-27, by wenzelm
fewer options;
2012-07-27, by wenzelm
tuned signature;
2012-07-27, by wenzelm
prefer explicit datatype Present.dump_mode;
2012-07-27, by wenzelm
simplified Session.name;
2012-07-27, by wenzelm
more precise imitation of usedir wrt. Session.name (cf. 45137257399a);
2012-07-27, by wenzelm
update docs
2012-07-27, by blanchet
extract Z3 unsat cores (for "z3_tptp")
2012-07-27, by blanchet
bring implementation of traditional encoding in line with paper
2012-07-27, by blanchet
further refinement of current/all_current status, which needs to be propagated through the hierarchy (see also Thy_Info.require_thys);
2012-07-26, by wenzelm
merged
2012-07-26, by wenzelm
[1] goes after any attributes
2012-07-26, by blanchet
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
2012-07-26, by blanchet
detect unknown options again
2012-07-26, by blanchet
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
2012-07-26, by blanchet
don't export technical theorems for MaSh
2012-07-26, by blanchet
repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-26, by blanchet
generate fact name in queries again + use ATP dependencies when possible
2012-07-26, by blanchet
proper all_current, which regards parent status as well;
2012-07-26, by wenzelm
more build options;
2012-07-26, by wenzelm
added session HOL-Tutorial;
2012-07-26, by wenzelm
recovered chapter on Presenting Theories;
2012-07-26, by wenzelm
avoid clash of Misc/pairs.thy and Types/Pairs.thy on case-insensible file-system;
2012-07-26, by wenzelm
proper input;
2012-07-26, by wenzelm
recovered latex job;
2012-07-26, by wenzelm
adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets;
2012-07-26, by wenzelm
more build options;
2012-07-26, by wenzelm
simplified Tutorial sessions;
2012-07-26, by wenzelm
proper arguments for old usedir;
2012-07-26, by wenzelm
more precise imports;
2012-07-26, by wenzelm
refined "document_dump_mode": "all", "tex+sty", "tex";
2012-07-26, by wenzelm
allow spaces in file names;
2012-07-26, by wenzelm
more files for session Pure;
2012-07-26, by wenzelm
discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;
2012-07-26, by wenzelm
tuned;
2012-07-26, by wenzelm
remove old output heaps, to ensure that result is valid wrt. check_stamps;
2012-07-26, by wenzelm
proper imports;
2012-07-26, by wenzelm
support session groups;
2012-07-26, by wenzelm
discontinued slightly odd session order, which did not quite work out;
2012-07-26, by wenzelm
tuned signature;
2012-07-26, by wenzelm
avoid clash of Advanced/simp.thy vs. Misc/simp.thy;
2012-07-25, by wenzelm
tuned signature;
2012-07-25, by wenzelm
actually check source vs. target stamps, based on information from log files;
2012-07-25, by wenzelm
tuned;
2012-07-25, by wenzelm
session specifications for doc-src, excluding TutorialI for now;
2012-07-25, by wenzelm
updated generated files;
2012-07-25, by wenzelm
clarified no_document situation;
2012-07-25, by wenzelm
no hardwired default for Proof General component -- its users can use init_component separately;
2012-07-25, by wenzelm
rail no longer exists;
2012-07-25, by wenzelm
some updates on "Building a repository version of Isabelle";
2012-07-25, by wenzelm
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
2012-07-25, by wenzelm
more standard session setup for WWW_Find;
2012-07-25, by wenzelm
read/write dependency information;
2012-07-24, by wenzelm
more files;
2012-07-24, by wenzelm
more build options;
2012-07-24, by wenzelm
merged
2012-07-24, by wenzelm
moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark
2012-07-24, by bulwahn
moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
2012-07-24, by bulwahn
reactivated HOL-NSA-Examples;
2012-07-24, by wenzelm
tuned order;
2012-07-24, by wenzelm
more build options;
2012-07-24, by wenzelm
tuned error;
2012-07-24, by wenzelm
more explicit checks during parsing;
2012-07-24, by wenzelm
more explicit document = false to reduce warnings;
2012-07-24, by wenzelm
pass parent_base_name, which is required for Session.init sanity check;
2012-07-24, by wenzelm
more session entries;
2012-07-24, by wenzelm
modernized imports;
2012-07-24, by wenzelm
more general notion of user ERROR (cf. 44f56fe01528);
2012-07-24, by wenzelm
tuned messages;
2012-07-24, by wenzelm
tuned message;
2012-07-24, by wenzelm
human-readable I/O error;
2012-07-24, by wenzelm
more session ROOT files;
2012-07-24, by wenzelm
tuned messages (cf. isabelle makeall);
2012-07-24, by wenzelm
tuned message;
2012-07-24, by wenzelm
actually negate "document" (cf. 7483aa690b4f);
2012-07-24, by wenzelm
clarified no_build vs. verbose;
2012-07-24, by wenzelm
clarified "document" again, eliminated redundant "no_document";
2012-07-24, by wenzelm
clarified build -n (no build);
2012-07-24, by wenzelm
added "document_dump_only" (cf. negated usedir -C);
2012-07-24, by wenzelm
more precise propagation of options: build, session, theories;
2012-07-24, by wenzelm
further imitation of ISABELLE_USEDIR_OPTIONS via options;
2012-07-24, by wenzelm
observe "condition";
2012-07-24, by wenzelm
observe "quick_and_dirty";
2012-07-24, by wenzelm
added "browser_info_remote" (cf. usedir -P);
2012-07-24, by wenzelm
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
2012-07-24, by wenzelm
timing for whole session;
2012-07-24, by wenzelm
tuned options;
2012-07-24, by wenzelm
timing is command line options, not system option;
2012-07-24, by wenzelm
clarified document options;
2012-07-24, by wenzelm
pass build options to ML;
2012-07-24, by wenzelm
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
2012-07-23, by wenzelm
provide explicit ISABELLE_PLATFORM32 as well;
2012-07-23, by wenzelm
merged
2012-07-23, by berghofe
set_vcs now derives prefix from fully qualified procedure / function name
2012-07-23, by berghofe
try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);
2012-07-23, by wenzelm
updated to Platypus 4.7;
2012-07-23, by wenzelm
merged
2012-07-23, by wenzelm
tuned;
2012-07-23, by wenzelm
clarified init_component: always liberal;
2012-07-23, by wenzelm
added system build mode: produce output in ISABELLE_HOME;
2012-07-23, by wenzelm
removed redundant check (cf. a8ed41b6280b);
2012-07-23, by wenzelm
pass ISABELLE_BROWSER_INFO as explicit argument;
2012-07-23, by wenzelm
removed some old/unused stuff;
2012-07-23, by wenzelm
updated smlnj settings;
2012-07-23, by wenzelm
cap the number of facts returned by MaSh
2012-07-23, by blanchet
remove MaSh junk associated with size functions
2012-07-23, by blanchet
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
2012-07-23, by blanchet
removed MaSh junk arising from primrec definitions
2012-07-23, by blanchet
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-23, by blanchet
tuning
2012-07-23, by blanchet
faster "save" operation
2012-07-23, by blanchet
include unknown local facts in MaSh
2012-07-23, by blanchet
ensure all calls to "mash" program are synchronous
2012-07-23, by blanchet
don't relearn old facts in Isar mode
2012-07-23, by blanchet
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
2012-07-23, by blanchet
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-07-23, by haftmann
more correct import
2012-07-23, by haftmann
merged
2012-07-22, by wenzelm
NEWS
2012-07-22, by haftmann
library theories for debugging and parallel computing using code generation towards Isabelle/ML
2012-07-22, by haftmann
also consider current working directory (cf. 3a5a5a992519)
2012-07-21, by haftmann
parallel scheduling of jobs;
2012-07-22, by wenzelm
tuned;
2012-07-22, by wenzelm
maintain set of source digests, including relevant parts of session entry;
2012-07-22, by wenzelm
determine source dependencies, relatively to preloaded theories;
2012-07-22, by wenzelm
propagate defined options;
2012-07-21, by wenzelm
disallow quotes in path specifications -- extra paranoia;
2012-07-21, by wenzelm
save image for inner nodes only;
2012-07-21, by wenzelm
some actual build function on ML side;
2012-07-21, by wenzelm
tuned -- no dependency on exit function;
2012-07-21, by wenzelm
more ML_System operations;
2012-07-21, by wenzelm
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
2012-07-21, by bulwahn
handling partiality in the case where the equality optimisation is applied
2012-07-21, by bulwahn
merged
2012-07-20, by wenzelm
updated File.find_files;
2012-07-20, by wenzelm
more abstract file system operations in Scala, corresponding to ML version;
2012-07-20, by wenzelm
eliminated obsolete session_manager.scala;
2012-07-20, by wenzelm
more explicit java.io.{File => JFile};
2012-07-20, by wenzelm
tune Mesh filter
2012-07-20, by blanchet
faster maximal node computation
2012-07-20, by blanchet
honor suggested MaSh weights
2012-07-20, by blanchet
use CVC3 and Yices by default if they are available and there are enough cores
2012-07-20, by blanchet