Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
added section "The Pure grammar" (incomplete version, based on old ref manual);
2008-11-13, by wenzelm
added section "Priority grammars" (variant from old ref manual);
2008-11-13, by wenzelm
added section "Co-regularity of type classes and arities" (variant from old ref manual);
2008-11-13, by wenzelm
minor tuning (according to old ref manual);
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
fixed/tuned syntax for attribute "tagged";
2008-11-13, by wenzelm
added pretty printing options (from old ref manual);
2008-11-13, by wenzelm
separate chapter "Inner syntax --- the term language";
2008-11-13, by wenzelm
updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13, by wenzelm
unified use of declaration environment with IsarImplementation;
2008-11-13, by wenzelm
ignore ThyOutput.source flag;
2008-11-13, by wenzelm
added bind_thm, bind_thms;
2008-11-13, by wenzelm
tuned section "Incorporating ML code";
2008-11-13, by wenzelm
tuned section "Oracles";
2008-11-13, by wenzelm
tuned section arrangement;
2008-11-13, by wenzelm
moved section "Proof method expressions" to proof chapter;
2008-11-13, by wenzelm
more on mixfix annotations (updated material from old ref manual);
2008-11-13, by wenzelm
tuned;
2008-11-13, by wenzelm
moved section "Document preparation" to front;
2008-11-13, by wenzelm
updated section "Markup via command tags";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
tuned "Markup commands";
2008-11-13, by wenzelm
tuned intro of "Document preparation";
2008-11-13, by wenzelm
reworked "Defining Theories";
2008-11-13, by wenzelm
removed Assert.thy
2008-11-13, by haftmann
dropped superfluos eval_conv
2008-11-13, by haftmann
moved assert to Heap_Monad.thy
2008-11-13, by haftmann
simproc for let
2008-11-13, by haftmann
improved handling of !!/==> for eval and normalization
2008-11-13, by haftmann
proper name morphisms for locales
2008-11-13, by haftmann
consider prefixes for name bindings of simprocs (a first approximation)
2008-11-13, by haftmann
diagnostic output for name bindings
2008-11-13, by haftmann
Some modifications in code for proving arities to make it work for datatype
2008-11-13, by berghofe
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-11-12, by krauss
restruced naming code in anticipation of introduction of name morphisms
2008-11-10, by haftmann
more verbose element printing
2008-11-10, by haftmann
clarified comment
2008-11-10, by haftmann
Added support for parametric datatypes.
2008-11-10, by berghofe
Streamlined functions for accessing information about atoms.
2008-11-10, by berghofe
Some more functions for accessing information about atoms.
2008-11-10, by berghofe
Made doc compatible with the system.
2008-11-10, by ballarin
clarified verbatim vs. typewriter
2008-11-10, by haftmann
using explicit interpretaton prefix in Name.binding (still on the surface)
2008-11-10, by haftmann
explicit interpretation prefix in Name.binding
2008-11-10, by haftmann
tuned
2008-11-10, by haftmann
exported codegen_preproc
2008-11-07, by haftmann
Minor cleanup.
2008-11-06, by ballarin
Keyword 'includes' gone.
2008-11-06, by ballarin
tuned
2008-11-06, by nipkow
added lemma
2008-11-06, by nipkow
Added second tiling example.
2008-11-06, by nipkow
cleaned
2008-11-06, by haftmann
tuned
2008-11-06, by haftmann
class morphism stemming from locale interpretation
2008-11-06, by haftmann
improved verbatim mechanism
2008-11-03, by haftmann
Theorem "_" is now stored with open derivation.
2008-10-31, by berghofe
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
2008-10-31, by berghofe
Replaced arbitrary by undefined.
2008-10-31, by berghofe
Dropped context element 'includes'.
2008-10-30, by ballarin
adapted to strict pattern discipline
2008-10-29, by haftmann
explicit check for pattern discipline before code translation
2008-10-29, by haftmann
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28, by ballarin
restored incremental code generation
2008-10-28, by haftmann
slightly tuned
2008-10-28, by haftmann
assert that no class parameter is used as constructor
2008-10-28, by haftmann
cleanup code default attribute
2008-10-28, by haftmann
removed includes
2008-10-28, by haftmann
making SMLNJ happy
2008-10-28, by haftmann
The metis method no longer fails because the theorem is too trivial
2008-10-28, by paulson
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-28, by ballarin
metis proof
2008-10-27, by paulson
New-style locale expressions with instantiation (new file expression.ML).
2008-10-27, by ballarin
Hide path in constant name (workaround).
2008-10-27, by ballarin
explicit history for equations; tuned
2008-10-27, by haftmann
slightly tuned
2008-10-27, by haftmann
added rudimentary code generation
2008-10-27, by haftmann
sup_bot and inf_top
2008-10-27, by haftmann
Extension of interface: declarations_of.
2008-10-27, by ballarin
simplified user-defined class syntax
2008-10-24, by haftmann
more clever module names for code generation
2008-10-24, by haftmann
"fun" gained a more uniform status
2008-10-24, by haftmann
simplified syntax for class parameters
2008-10-24, by haftmann
tuned
2008-10-24, by haftmann
new classes "top" and "bot"
2008-10-24, by haftmann
tuned proof
2008-10-24, by haftmann
more clever module name aliasses for code generation
2008-10-24, by haftmann
"arbitrary" merely abbreviates undefined
2008-10-24, by haftmann
subst is a proper axiom again
2008-10-24, by haftmann
updated
2008-10-24, by haftmann
explicit namings for generated code
2008-10-24, by haftmann
Thm.get_def;
2008-10-23, by wenzelm
Thm.def_name;
2008-10-23, by wenzelm
multithreading support only for polyml-5.2.1 or later;
2008-10-23, by wenzelm
renamed get_axiom_i to axiom, removed obsolete get_axiom;
2008-10-23, by wenzelm
renamed Thm.get_axiom_i to Thm.axiom;
2008-10-23, by wenzelm
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23, by wenzelm
adapted Susp.peek;
2008-10-23, by wenzelm
thread-safe version, with non-critical evaluation;
2008-10-23, by wenzelm
do not open Susp;
2008-10-23, by wenzelm
switched parallel sessions to polyml-5.2.1;
2008-10-23, by wenzelm
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-10-23, by wenzelm
updated to 5.2.1;
2008-10-22, by wenzelm
prove_instantiation_exit combinators
2008-10-22, by haftmann
added meet_sort_typ
2008-10-22, by haftmann
tuned
2008-10-22, by haftmann
code identifier namings are no longer imperative
2008-10-22, by haftmann
tuned typedef interface
2008-10-22, by haftmann
slightly tuned
2008-10-22, by haftmann
fixed
2008-10-22, by haftmann
less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21, by wenzelm
JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21, by wenzelm
make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21, by wenzelm
Added nominal_inductive2.
2008-10-21, by berghofe
Example for using the generalized version of nominal_inductive.
2008-10-21, by berghofe
Added theory W.
2008-10-21, by berghofe
More general, still experimental version of nominal_inductive for
2008-10-21, by berghofe
Added nominal_inductive2.ML
2008-10-21, by berghofe
added jEdit settings;
2008-10-21, by wenzelm
tuned usage line;
2008-10-21, by wenzelm
Isabelle/jEdit interface wrapper.
2008-10-21, by wenzelm
join results in isolation;
2008-10-21, by wenzelm
join_results: allow CRITICAL join of finished futures;
2008-10-21, by wenzelm
Future.join_result;
2008-10-21, by wenzelm
added Future.enabled check;
2008-10-21, by wenzelm
ThyOutput: export some auxiliary operations;
2008-10-21, by wenzelm
fixed proof
2008-10-20, by nipkow
added lemmas
2008-10-20, by nipkow
Names of variables in perm_eqs are now chosen more carefully to avoid
2008-10-19, by berghofe
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-19, by berghofe
datatype_codegen now checks name of result type of constructor
2008-10-19, by berghofe
run a program in a modified environment;
2008-10-19, by wenzelm
reactivated HOL-Matrix;
2008-10-17, by wenzelm
tuned
2008-10-17, by haftmann
filled remaining gaps
2008-10-17, by haftmann
added type antiquotation
2008-10-17, by haftmann
tuned;
2008-10-16, by wenzelm
added dep for Concurrent/ROOT.ML;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
removed Locales;
2008-10-16, by wenzelm
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16, by wenzelm
added translations for SORT_CONSTRAINT
2008-10-16, by wenzelm
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added make;
2008-10-16, by wenzelm
maintain sort occurrences of declared terms;
2008-10-16, by wenzelm
added weaken_sorts;
2008-10-16, by wenzelm
added make, minimal_sorts;
2008-10-16, by wenzelm
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16, by wenzelm
added check_shyps, which reject pending sort hypotheses;
2008-10-16, by wenzelm
Drule.norm_hhf_eqs;
2008-10-16, by wenzelm
prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
avoid accidental dependency of automated proof on sort equiv;
2008-10-16, by wenzelm
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16, by wenzelm
avoid CRITICAL with_path;
2008-10-16, by wenzelm
rewrite more proofs in Isar style
2008-10-16, by huffman
Removed ex/Locales.thy.
2008-10-16, by ballarin
More occurrences of 'includes' gone.
2008-10-16, by ballarin
Removed outdated locales tutorial.
2008-10-16, by ballarin
correct rounding
2008-10-16, by haftmann
circumvent some TeX problem
2008-10-16, by haftmann
only test HOL image for smlnj
2008-10-16, by kleing
tuned;
2008-10-15, by wenzelm
tuned;
2008-10-15, by wenzelm
generic ATP manager based on threads (by Fabian Immler);
2008-10-15, by wenzelm
added sledgehammer etc.;
2008-10-15, by wenzelm
removed obsolete Complex sessions;
2008-10-15, by wenzelm
figure for adaption
2008-10-15, by haftmann
Removed 'includes' (fixed).
2008-10-15, by ballarin
Removed 'includes'.
2008-10-15, by ballarin
give more time to do inital loggin and settings read
2008-10-15, by kleing
log start of test session
2008-10-15, by kleing
tuned interfaces -- plain prover function, without thread;
2008-10-14, by wenzelm
add_prover: plain prover function, without thread;
2008-10-14, by wenzelm
tuned AtpWrapper interfaces;
2008-10-14, by wenzelm
continued codegen tutorial
2008-10-14, by haftmann
renamed AtpThread to AtpWrapper;
2008-10-14, by wenzelm
adding preferences is now permissive;
2008-10-14, by wenzelm
tuned;
2008-10-14, by wenzelm
adding preferences is now permissive, no error handling here;
2008-10-14, by wenzelm
CRITICAL access to preferences;
2008-10-14, by wenzelm
export generic_pref etc.;
2008-10-14, by wenzelm
renamed kill_all to kill, in conformance with atp_kill command;
2008-10-14, by wenzelm
tuned comments;
2008-10-14, by wenzelm
added lemma
2008-10-14, by nipkow
Added liveness analysis
2008-10-14, by nipkow
info: back to plain printing;
2008-10-14, by wenzelm
added min_elem, upto;
2008-10-14, by wenzelm
added value;
2008-10-14, by wenzelm
simplified synchronized variable access;
2008-10-14, by wenzelm
State variables with synchronized access.
2008-10-13, by wenzelm
added generic combinator for synchronized evaluation (formerly in future.ML);
2008-10-13, by wenzelm
simplified implementation using Synchronized.var;
2008-10-13, by wenzelm
SimpleThread.synchronized;
2008-10-13, by wenzelm
added Concurrent/synchronized.ML;
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
tuned output;
2008-10-13, by wenzelm
tuned
2008-10-13, by haftmann
tuned
2008-10-13, by urbanc
change DISTPREFIX to not use yet another filesystem
2008-10-11, by kleing
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
`code func` now just `code`
2008-10-10, by haftmann
some adaption
2008-10-10, by haftmann
using tikz pictures
2008-10-10, by haftmann
tuned default rules of (dvd)
2008-10-10, by haftmann
replaced str_of by general peek;
2008-10-09, by wenzelm
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-10-09, by wenzelm
fixed spelling;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
Multithreading.enabled;
2008-10-09, by wenzelm
moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-09, by wenzelm
added invalidate_group;
2008-10-09, by wenzelm
added fail-safe interrupt;
2008-10-09, by wenzelm
subject to Multithreading.enabled;
2008-10-09, by wenzelm
future result: Interrupt invalidates group, but pretends success otherwise;
2008-10-09, by wenzelm
added future_scheduler flag (tmp!), from skip_proofs.ML;
2008-10-09, by wenzelm
Dummy version of parallel list combinators -- plain sequential evaluation.
2008-10-09, by wenzelm
added Concurrent/par_list_dummy.ML;
2008-10-09, by wenzelm
improved performance of skolem cache, due to parallel map;
2008-10-09, by wenzelm
SimpleThread.interrupt;
2008-10-09, by wenzelm
report: back to single message;
2008-10-09, by wenzelm
added section label;
2008-10-09, by wenzelm
tuned
2008-10-09, by haftmann
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
2008-10-09, by kleing
removed legacy |>>>
2008-10-09, by haftmann
established canonical argument order in SML code generators
2008-10-09, by haftmann
established canonical argument order
2008-10-09, by haftmann
made SMLNJ happy
2008-10-09, by haftmann
less tracing;
2008-10-08, by wenzelm
Future.joint_results is already uninterruptible;
2008-10-08, by wenzelm
more careful handling of group interrupts;
2008-10-08, by wenzelm
use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;
2008-10-08, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip