isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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