Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-960
+960
+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 future_scheduler (from thy_info.ML);
2008-09-25, by wenzelm
simplified promise;
2008-09-25, by wenzelm
simplified Thm.promise;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
2008-09-25, by wenzelm
circumvent problem with code redundancy
2008-09-25, by haftmann
clarifed redundancy policy
2008-09-25, by haftmann
tuned comments;
2008-09-25, by wenzelm
added release_results;
2008-09-25, by wenzelm
abtract types: plain datatype with opaque signature matching;
2008-09-25, by wenzelm
prove: error with original thread position;
2008-09-25, by wenzelm
explicit type OrdList.T;
2008-09-25, by wenzelm
(temporary workaround)
2008-09-25, by haftmann
(temporal deactivation)
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
map_force
2008-09-25, by haftmann
matchess
2008-09-25, by haftmann
burrow_fst
2008-09-25, by haftmann
discontinued special treatment of op = vs. eq_class.eq
2008-09-25, by haftmann
report: produce individual status messages;
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
init: OuterKeyword.report;
2008-09-24, by wenzelm
prove_multi: immediate;
2008-09-23, by wenzelm
added promise_result, prove_promise;
2008-09-23, by wenzelm
Corrected call of SUBPROOF in coherent_tac that used wrong context.
2008-09-23, by berghofe
fixed outer syntax
2008-09-23, by haftmann
case default fallback for NBE
2008-09-23, by haftmann
fixed quickcheck parameter syntax
2008-09-23, by haftmann
renamed rtype to typerep
2008-09-23, by haftmann
added fold_rev;
2008-09-23, by wenzelm
added del_node, which is more efficient for sparse graphs;
2008-09-23, by wenzelm
IntGraph.del_node;
2008-09-23, by wenzelm
join_results: special case for empty list, works without multithreading;
2008-09-23, by wenzelm
added dest_deriv, removed external type deriv;
2008-09-23, by wenzelm
added conditional add_oracles, keep oracles_of_proof private;
2008-09-23, by wenzelm
Thm.proof_of;
2008-09-23, by wenzelm
Added coherent logic prover.
2008-09-22, by berghofe
New prover for coherent logic.
2008-09-22, by berghofe
Added setup for coherent logic prover.
2008-09-22, by berghofe
Added examples for coherent logic prover.
2008-09-22, by berghofe
Examples for coherent logic prover.
2008-09-22, by berghofe
made the perm_simp tactic to understand options such as (no_asm)
2008-09-22, by urbanc
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
added is_finished;
2008-09-22, by wenzelm
added Promise constructor, which is similar to Oracle but may be replaced later;
2008-09-22, by wenzelm
removed deriv.ML which is now incorporated into thm.ML;
2008-09-22, by wenzelm
added reject_draft;
2008-09-22, by wenzelm
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
generic quickcheck framework
2008-09-22, by haftmann
TEMPORARY: make batch run happy
2008-09-22, by haftmann
absolute Library path
2008-09-22, by haftmann
different session branches for HOL-Plain vs. Plain
2008-09-22, by haftmann
temporary workaround for class constants
2008-09-22, by haftmann
corrected sort intersection
2008-09-22, by haftmann
some steps towards generic quickcheck framework
2008-09-22, by haftmann
fixed headers
2008-09-22, by haftmann
added some fragments from website
2008-09-22, by haftmann
made SML/NJ happy;
2008-09-20, by wenzelm
Isar toplevel editor model.
2008-09-19, by wenzelm
future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-19, by wenzelm
output_sync is now public;
2008-09-19, by wenzelm
added props_text (from isar_syn.ML);
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
added Isar/isar.scala;
2008-09-19, by wenzelm
avoid using implicit assumptions
2008-09-19, by huffman
add theory graph to ZF document
2008-09-19, by huffman
made SMLNJ happy
2008-09-19, by haftmann
jar: include sources;
2008-09-18, by wenzelm
tuned;
2008-09-18, by wenzelm
eval_term: CRITICAL due to eval_result;
2008-09-18, by wenzelm
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
2008-09-18, by wenzelm
updated generated file;
2008-09-18, by wenzelm
simplified oracle interface;
2008-09-18, by wenzelm
show: non-critical testing;
2008-09-18, by wenzelm
added deriv.ML: Abstract derivations based on raw proof terms.
2008-09-18, by wenzelm
termination prover for "fun" can be configured using context data.
2008-09-18, by krauss
updated generated file;
2008-09-18, by wenzelm
unchecked $ISABELLE_HOME_USER/etc/settings;
2008-09-18, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
threads work only for Poly/ML 5.2 or later;
2008-09-17, by wenzelm
* ML bindings produced via Isar commands are stored within the Isar context.
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
added inherit_env;
2008-09-17, by wenzelm
added map_contexts;
2008-09-17, by wenzelm
ML_prf: inherit env for all contexts within the proof;
2008-09-17, by wenzelm
shutdown only if Multithreading.available;
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
explicit handling of ML environment within generic context;
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
ML name space -- dummy version of Poly/ML 5.2 facility.
2008-09-17, by wenzelm
added ML-Systems/ml_name_space.ML;
2008-09-17, by wenzelm
use ML_prf within proofs;
2008-09-17, by wenzelm
local @{context};
2008-09-17, by wenzelm
moved global ML bindings to global place;
2008-09-17, by wenzelm
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
wf_finite_psubset[simp], in_finite_psubset[simp]
2008-09-17, by krauss
Public interface to interpretation morphism.
2008-09-17, by ballarin
moved term_of syntax to separate theory
2008-09-17, by haftmann
removed obsolete theory
2008-09-17, by haftmann
added quickcheck.ML
2008-09-17, by haftmann
tuned comments;
2008-09-16, by wenzelm
multithreading for Poly/ML 5.1 is no longer supported;
2008-09-16, by wenzelm
tuned;
2008-09-16, by wenzelm
updated system manual;
2008-09-16, by wenzelm
Proof General / Emacs interface wrapper;
2008-09-16, by wenzelm
Proof General: option -I is obsolete;
2008-09-16, by wenzelm
added PROOFGENERAL_HOME;
2008-09-16, by wenzelm
separate emacs tool for Proof General / Emacs;
2008-09-16, by wenzelm
added quickcheck stub
2008-09-16, by haftmann
removed babel again
2008-09-16, by haftmann
celver code lemma avoid type ambiguity problem with Haskell
2008-09-16, by haftmann
a sophisticated char/nibble conversion combinator
2008-09-16, by haftmann
moved term_of syntax to separate theory
2008-09-16, by haftmann
SimpleThread.fork;
2008-09-16, by wenzelm
Simplified thread fork interface.
2008-09-16, by wenzelm
added Concurrent/simple_thread.ML;
2008-09-16, by wenzelm
updated generated file;
2008-09-16, by wenzelm
misc tuning and modernization;
2008-09-16, by wenzelm
check setting and tool;
2008-09-16, by wenzelm
Clearer separation of interpretation frontend and backend.
2008-09-16, by ballarin
No interpretation of locale with dangling type frees.
2008-09-16, by ballarin
Do not rely on locale assumption in interpretation.
2008-09-16, by ballarin
The metis method now fails in the usual manner, rather than raising an exception,
2008-09-16, by paulson
Fixed typo in locale declaration.
2008-09-16, by ballarin
added babel
2008-09-16, by haftmann
explicit size of characters
2008-09-16, by haftmann
dropped superfluous code lemmas
2008-09-16, by haftmann
evaluation using code generator
2008-09-16, by haftmann
generic value command
2008-09-16, by haftmann
converted symbols.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
converted misc.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
generated files;
2008-09-15, by wenzelm
converted present.tex;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
load underscore package after iman etc.;
2008-09-15, by wenzelm
tuned comment;
2008-09-15, by wenzelm
added formal markup for setting, executable, tool;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
converted basics.tex to theory file;
2008-09-15, by wenzelm
added isatt markup;
2008-09-15, by wenzelm
New outline for codegen tutorial -- draft
2008-09-14, by haftmann
added extern_fact (local or global);
2008-09-12, by wenzelm
print raw (internal) result names;
2008-09-12, by wenzelm
more procise printing of fact names;
2008-09-12, by wenzelm
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-12, by wenzelm
cancel, shutdown: notify_all;
2008-09-11, by wenzelm
finish: Future.shutdown last;
2008-09-11, by wenzelm
eliminated requests, use global state variables uniformly;
2008-09-11, by wenzelm
finish: Future.shutdown;
2008-09-11, by wenzelm
added is_empty;
2008-09-11, by wenzelm
shutdown: global join-and-shutdown operation;
2008-09-11, by wenzelm
added focus, which indicates a particular collection of high-priority tasks;
2008-09-11, by wenzelm
some general notes on future values;
2008-09-11, by wenzelm
separate Concurrent/ROOT.ML;
2008-09-11, by wenzelm
Parallel list combinators.
2008-09-11, by wenzelm
added Concurrent/par_list.ML;
2008-09-11, by wenzelm
added interrupt_task (external id);
2008-09-10, by wenzelm
tuned;
2008-09-10, by wenzelm
future_schedule: uninterruptible join;
2008-09-10, by wenzelm
added future_scheduler (default false);
2008-09-10, by wenzelm
replaced join_all by join_results, which returns Exn.results;
2008-09-10, by wenzelm
workers: explicit activity flag;
2008-09-10, by wenzelm
future: allow explicit group;
2008-09-10, by wenzelm
cancel: invalidate group implicitly, via bool ref;
2008-09-10, by wenzelm
auto_flush: uniform block buffering for all output streams;
2008-09-10, by wenzelm
auto_flush stdout, stderr as well;
2008-09-09, by wenzelm
proper values of no_interrupts, regular_interrupts;
2008-09-09, by wenzelm
cancel: check_scheduler;
2008-09-09, by wenzelm
simplified dequeue: provide Thread.self internally;
2008-09-09, by wenzelm
eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09, by wenzelm
export get_first from underlying table;
2008-09-09, by wenzelm
out_stream: block-buffered, with separate autoflush thread (every 50ms);
2008-09-09, by wenzelm
babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
2008-09-09, by wenzelm
added comment
2008-09-09, by nipkow
human-readable printing of TaskQueue.task/group;
2008-09-09, by wenzelm
* Changed defaults for unify configuration options;
2008-09-09, by wenzelm
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
2008-09-09, by wenzelm
job: explicit 'ok' status -- false for canceled jobs;
2008-09-09, by wenzelm
Overall exception handler in order to insulate our users from low-level bugs.
2008-09-09, by paulson
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-09-09, by paulson
Increasing the default limits in order to prevent unnecessary failures.
2008-09-09, by paulson
send: broadcast condition while locked!
2008-09-08, by wenzelm
proper signature constraint;
2008-09-08, by wenzelm
tuned Mailbox.send;
2008-09-08, by wenzelm
removed unused sync_interrupts;
2008-09-08, by wenzelm
moved thread data to future.ML (again);
2008-09-08, by wenzelm
more interrupt operations;
2008-09-08, by wenzelm
moved task, thread_data, group, queue to task_queue.ML;
2008-09-08, by wenzelm
Ordered queue of grouped tasks.
2008-09-08, by wenzelm
added Concurrent/task_queue.ML;
2008-09-08, by wenzelm
await: SYNCHRONIZED wait!
2008-09-08, by wenzelm
tuned check_cache;
2008-09-08, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
opaque signature constraint abstracts local type abbrev;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
added change_result;
2008-09-07, by wenzelm
Functional threads as future values.
2008-09-07, by wenzelm
added Concurrent/future.ML;
2008-09-07, by wenzelm
Default (mostly dummy) implementation of thread structures.
2008-09-07, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2008-09-07, by wenzelm
*** empty log message ***
2008-09-07, by wenzelm
explicit use of universal.ML and dummy_thread.ML;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
send: broadcast to all waiting threads;
2008-09-07, by wenzelm
added ML-Systems/thread_dummy.ML;
2008-09-07, by wenzelm
dropped "run" marker in monad syntax
2008-09-06, by haftmann
multithreading.ML provides dummy thread structures;
2008-09-05, by wenzelm
different bookkeeping for code equations
2008-09-05, by haftmann
renamed structure CodeTarget to Code_Target
2008-09-05, by haftmann
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
2008-09-05, by huffman
proper header;
2008-09-04, by wenzelm
added receive_timeout;
2008-09-04, by wenzelm
check WRAPPER_OUTPUT node type;
2008-09-04, by wenzelm
init: disallow "" as out stream;
2008-09-04, by wenzelm
fixed deps: no Concurrent/receiver.ML yet;
2008-09-04, by wenzelm
Concurrent message exchange via mailbox -- with unbounded queueing.
2008-09-04, by wenzelm
added Concurrent/mailbox.ML;
2008-09-04, by wenzelm
reorganize subsections
2008-09-04, by huffman
rename INF_drop_prefix to INFM_drop_prefix
2008-09-04, by huffman
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
2008-09-04, by huffman
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
2008-09-04, by huffman
tuned signature;
2008-09-04, by wenzelm
added General/queue.ML;
2008-09-04, by wenzelm
Efficient queues.
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML
2008-09-04, by wenzelm
multithreading.ML provides dummy thread structures;
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML;
2008-09-04, by wenzelm
provide dummy thread structures, including proper Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Scheduling -- multiple threads working on a queue of tasks.
2008-09-04, by wenzelm
added Concurrent/schedule.ML;
2008-09-04, by wenzelm
update tags
2008-09-03, by convert-repo
use /home/isabelle/mercurial/bin/hg wrapper;
2008-09-03, by wenzelm
exclude large .mov files;
2008-09-03, by wenzelm
simplified add_axiom: no hyps;
2008-09-03, by wenzelm
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-03, by wenzelm
axiomatization is now global-only;
2008-09-03, by wenzelm
added const_decl;
2008-09-03, by wenzelm
simplified specify_const: canonical args, global deps;
2008-09-03, by wenzelm
declare_const: Name.binding, store/report position;
2008-09-03, by wenzelm
Sign.declare_const: Name.binding;
2008-09-03, by wenzelm
removed ex/Puzzle
2008-09-03, by nipkow
added qualified: string -> binding -> binding;
2008-09-03, by wenzelm
Name.qualified;
2008-09-03, by wenzelm
theorem dependency hook: check previous state;
2008-09-03, by wenzelm
added pos_of;
2008-09-03, by wenzelm
-> AFP
2008-09-03, by nipkow
simplified Toplevel.add_hook: cover successful transactions only;
2008-09-03, by wenzelm
retired Ben Porter's DenumRat in favour of the shorter proof in
2008-09-03, by kleing
made SML/NJ happy;
2008-09-02, by wenzelm
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
2008-09-02, by wenzelm
* Generic Toplevel.add_hook interface allows to analyze the result of
2008-09-02, by wenzelm
Replaced Library/NatPair by Nat_Int_Bij.
2008-09-02, by nipkow
added new_thms_deps (operates on global facts, some name_hint approximation);
2008-09-02, by wenzelm
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
2008-09-02, by wenzelm
added add_hook interface for post-transition hooks;
2008-09-02, by wenzelm
tuned;
2008-09-02, by wenzelm
ProofDisplay.print_results;
2008-09-02, by wenzelm
no pervasive bindings;
2008-09-02, by wenzelm
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
2008-09-02, by nipkow
distributed literal code generation out of central infrastructure
2008-09-02, by haftmann
* Result facts now refer to the *full* internal name;
2008-09-02, by wenzelm
* Name bindings in higher specification mechanisms;
2008-09-02, by wenzelm
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-09-02, by wenzelm
updated generated file;
2008-09-02, by wenzelm
Interpretation commands no longer accept interpretation attributes.
2008-09-02, by ballarin
type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
added binding;
2008-09-02, by wenzelm
added fixed_decl, fact_decl, local_fact_decl;
2008-09-02, by wenzelm
name_thm etc.: pass position;
2008-09-02, by wenzelm
added type binding -- generic name bindings;
2008-09-02, by wenzelm
name/var morphism operates on Name.binding;
2008-09-02, by wenzelm
adapted to class instantiation compliance
2008-09-02, by haftmann
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
2008-09-01, by nipkow
renamed lemma
2008-09-01, by nipkow
moved more lemmas here from AFP/Integration/Rats
2008-09-01, by nipkow
moved lemma into SetInterval where it belongs
2008-09-01, by nipkow
cleaned up code generation for {.._} and {..<_}
2008-09-01, by nipkow
*** empty log message ***
2008-09-01, by nipkow
extended interface to preferences to allow adding new ones
2008-09-01, by nipkow
Prover is set via menu now
2008-09-01, by nipkow
restructured code generation of literals
2008-09-01, by haftmann
IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
2008-08-29, by wenzelm
init: more explicit protocol of open/remove rendezvous;
2008-08-29, by wenzelm
use hardwired /tmp -- fifo only work on local file-system;
2008-08-29, by wenzelm
separate module for code output
2008-08-29, by haftmann
fixed names of class assumptions
2008-08-29, by haftmann
dropped parameter prefix for class theorems
2008-08-29, by haftmann
added charset (from isabelle_process.scala);
2008-08-28, by wenzelm
moved charset to isabelle_system.scala;
2008-08-28, by wenzelm
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
2008-08-28, by wenzelm
restructured and split code serializer module
2008-08-28, by haftmann
no parameter prefix for class interpretation
2008-08-28, by haftmann
updated
2008-08-28, by haftmann
tuned fold_lines;
2008-08-28, by wenzelm
fold_lines: simplified, more efficient due to String.fields;
2008-08-28, by wenzelm
rm fifo after open;
2008-08-28, by wenzelm
dummy setup for completion;
2008-08-28, by wenzelm
create named pipe;
2008-08-28, by wenzelm
added is_cygwin;
2008-08-28, by wenzelm
join stdout/stderr, eliminated Kind.STDERR;
2008-08-28, by wenzelm
explicit output stream, typically a named pipe;
2008-08-28, by wenzelm
refined option -W: output stream;
2008-08-28, by wenzelm
more function -> fun
2008-08-28, by krauss
quicksort: function -> fun
2008-08-28, by krauss
corrected some typos
2008-08-28, by krauss
fixed atom_to_xml: literal "name" attribute;
2008-08-28, by wenzelm
exported atom_to_xml;
2008-08-28, by wenzelm
changed Markup print mode to YXML -- explicitly decode messages before being issued;
2008-08-28, by wenzelm
tuned;
2008-08-28, by wenzelm
present_token: disable print_mode, which is YXML now;
2008-08-28, by wenzelm
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;
2008-08-28, by wenzelm
removed obsolete XML.Output workaround;
2008-08-28, by wenzelm
added get_int;
2008-08-28, by wenzelm
removed obsolete get_string;
2008-08-28, by wenzelm
removed obsolete ProofGeneral/pgml_isabelle.ML;
2008-08-28, by wenzelm
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
2008-08-27, by huffman
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
load buffer.ML before file.ML;
2008-08-27, by wenzelm
replaced find_substring by first_field;
2008-08-27, by wenzelm
Consistent naming of theorems in interpretation.
2008-08-27, by ballarin
simplified parse_attrib (find_substring instead of space_explode);
2008-08-27, by wenzelm
added find_substring;
2008-08-27, by wenzelm
added HOL/ex/Numeral.thy
2008-08-27, by haftmann
get rid of tabs;
2008-08-27, by wenzelm
Property lists.
2008-08-27, by wenzelm
added General/properties.ML;
2008-08-27, by wenzelm
type Properties.T;
2008-08-27, by wenzelm
proper error message
2008-08-27, by haftmann
proper handling of type variabl names
2008-08-27, by haftmann
completing arities after subclass instance
2008-08-27, by haftmann
untabification
2008-08-27, by haftmann
tuned code generator setup
2008-08-27, by haftmann
added equivariance lemmas for ex1 and the
2008-08-27, by urbanc
add lemmas about Rats similar to those about Reals
2008-08-27, by huffman
move real_vector class proofs into vector_space and group_hom locales
2008-08-26, by huffman
added distributivity of relation composition over union [simp]
2008-08-26, by krauss
tuned append;
2008-08-26, by wenzelm
command: symbols.encode;
2008-08-26, by wenzelm
Reorganisation of registration code.
2008-08-26, by ballarin
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
2008-08-26, by krauss
purge classes after compilation;
2008-08-26, by wenzelm
renamed Isabelle-repository to isabelle;
2008-08-26, by wenzelm
Defined rationals (Rats) globally in Rational.
2008-08-26, by nipkow
replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
2008-08-26, by wenzelm
moved new Symbol.Interpretation into plugin;
2008-08-25, by wenzelm
promoted to EBPlugin;
2008-08-25, by wenzelm
explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;
2008-08-25, by wenzelm
tuned;
2008-08-25, by wenzelm
isabelle process: pick options/args from properties;
2008-08-25, by wenzelm
removed unused ConsolePlugin dependency;
2008-08-25, by wenzelm
simplified exceptions: use plain error function / RuntimeException;
2008-08-25, by wenzelm
added try_result;
2008-08-25, by wenzelm
misc reorganization;
2008-08-24, by wenzelm
Kind: added is_control;
2008-08-24, by wenzelm
get: allow null;
2008-08-24, by wenzelm
misc tuning of names;
2008-08-24, by wenzelm
rearranged source files;
2008-08-24, by wenzelm
init_message: class markup in message body, not header;
2008-08-24, by wenzelm
repackaged as isabelle.jedit;
2008-08-24, by wenzelm
untabify: silently turn tab into space if column information is unavailable;
2008-08-24, by wenzelm
corrected cache handling for class operations
2008-08-24, by haftmann
default replaces arbitrary
2008-08-24, by haftmann
tuned import order
2008-08-24, by haftmann
activated \<A>, \<a>, \<AA>, \<aa>;
2008-08-24, by wenzelm
* Isabelle/lib/classes/Pure.jar;
2008-08-23, by wenzelm
jars: removed obsolete Java process wrapper (cf. new Pure.jar);
2008-08-23, by wenzelm
obsolete;
2008-08-23, by wenzelm
obsolete -- superceded by Pure.jar (Scala version);
2008-08-23, by wenzelm
updated to Pure.jar;
2008-08-23, by wenzelm
added exec;
2008-08-23, by wenzelm
moved class Result into static object, removed dynamic tree method;
2008-08-23, by wenzelm
symbolic message markup;
2008-08-23, by wenzelm
renamed Markup.MALFORMED to Markup.BAD;
2008-08-23, by wenzelm
added position, messages;
2008-08-23, by wenzelm
added messages and process information;
2008-08-23, by wenzelm
Position properties.
2008-08-23, by wenzelm
added General/position.scala;
2008-08-23, by wenzelm
adapted to new IsabelleProcess from Pure.jar;
2008-08-23, by wenzelm
include ../../classes/Pure.jar;
2008-08-23, by wenzelm
added const Rational
2008-08-23, by nipkow
YXML.parse_failsafe;
2008-08-23, by wenzelm
shell_prefix: physical /bin/env on Cygwin;
2008-08-23, by wenzelm
removed full_markup mode (default);
2008-08-23, by wenzelm
added parse_failsafe;
2008-08-23, by wenzelm
refer to symbolic Markup;
2008-08-23, by wenzelm
Common markup elements.
2008-08-23, by wenzelm
added General/markup.scala;
2008-08-23, by wenzelm
BadVariable: toString;
2008-08-23, by wenzelm
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
2008-08-23, by wenzelm
append_string: proper backslash in character escapes;
2008-08-23, by wenzelm
added getenv;
2008-08-23, by wenzelm
tuned;
2008-08-23, by wenzelm
Isabelle outer syntax.
2008-08-23, by wenzelm
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
2008-08-23, by wenzelm
Isabelle process management -- always reactive due to multi-threaded I/O.
2008-08-23, by wenzelm
renamed DOM to document, add xml version and optional stylesheets;
2008-08-23, by wenzelm
tuned comments;
2008-08-22, by wenzelm
parse_attrib: proper index of name end!
2008-08-21, by wenzelm
tuned parse performance: avoid splitting terminal Y chunk;
2008-08-21, by wenzelm
parse_attrib: more efficient due to indexOf('=');
2008-08-21, by wenzelm
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
2008-08-21, by wenzelm
tuned comment;
2008-08-21, by wenzelm
added iterator over content;
2008-08-21, by wenzelm
proper ISABELLE_ROOT_JVM on Cygwin;
2008-08-21, by wenzelm
pattern: proper "." not "[.]"!
2008-08-21, by wenzelm
recode: proper result for unmatched symbols;
2008-08-21, by wenzelm
more robust pattern: look at longer matches first, added catch-all case;
2008-08-21, by wenzelm
added get_setting;
2008-08-21, by wenzelm
read_symbols: proper IsabelleSystem.platform_path;
2008-08-21, by wenzelm
added ISABELLE_ROOT_JVM;
2008-08-21, by wenzelm
Theorem on polynomial division and lemmas.
2008-08-18, by ballarin
removed parse_element -- no longer fits to liberal parse!
2008-08-17, by wenzelm
Minimalistic XML tree values.
2008-08-17, by wenzelm
Efficient text representation of XML trees.
2008-08-17, by wenzelm
added General/xml.scala, General/yxml.scala;
2008-08-17, by wenzelm
decode escaped symbols as well;
2008-08-17, by wenzelm
tuned Recoder;
2008-08-16, by wenzelm
more private fields;
2008-08-16, by wenzelm
jar: invoke scaladoc;
2008-08-16, by wenzelm
tuned comments;
2008-08-16, by wenzelm
use scala.collection.jcl.HashMap, which seems to be more efficient;
2008-08-16, by wenzelm
jar target: removed jvmpath -- does not work on Linux!?
2008-08-16, by wenzelm
add scala-library.jar if available;
2008-08-16, by wenzelm
jar target: jvmpath;
2008-08-16, by wenzelm
Isabelle system support.
2008-08-16, by wenzelm
reading symbol interpretation tables;
2008-08-16, by wenzelm
added Tools/isabelle_system.scala;
2008-08-16, by wenzelm
removed unused usage;
2008-08-16, by wenzelm
more robust handling of directory layout variants;
2008-08-16, by wenzelm
refined scala/java wrappers via isatool;
2008-08-16, by wenzelm
tuned abbrevs;
2008-08-16, by wenzelm
added ISABELLE_SCALA, ISABELLE_JAVA;
2008-08-16, by wenzelm
added ISABELLE_HOME_JVM;
2008-08-15, by wenzelm
proper jvmpath for cygwin;
2008-08-15, by wenzelm
proper RC;
2008-08-15, by wenzelm
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
2008-08-15, by wenzelm
refined JVM path wrappers;
2008-08-15, by wenzelm
added JVM components (Scala or Java);
2008-08-15, by wenzelm
tuned;
2008-08-15, by wenzelm
jars: build Pure.jar;
2008-08-15, by wenzelm
scan: proper recovery for escaped \\< symbols;
2008-08-15, by wenzelm
basic setup for Scala material;
2008-08-15, by wenzelm
Basic support for Isabelle symbols.
2008-08-15, by wenzelm
added some abbrevs;
2008-08-15, by wenzelm
removed redundant "symbol" property;
2008-08-15, by wenzelm
Default interpretation of some Isabelle symbols.
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
added ML_antiq, doc_antiq;
2008-08-15, by wenzelm
added README;
2008-08-15, by wenzelm
generated truetype font;
2008-08-15, by wenzelm
The Jerusalem font from 2004 -- unicode version.
2008-08-15, by wenzelm
args: explicit groups for file_name, theory_name;
2008-08-15, by wenzelm
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
2008-08-15, by wenzelm
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
2008-08-15, by wenzelm
token_kind: add Space, Comment;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
output_markup: check Markup.is_none;
2008-08-15, by wenzelm
added is_none;
2008-08-15, by wenzelm
Args.name_source(_position) for proper position information;
2008-08-15, by wenzelm
[source=false] for quoted antiquotation avoids quote-escapes in output;
2008-08-14, by wenzelm
report antiquotations;
2008-08-14, by wenzelm
tuned;
2008-08-14, by wenzelm
report ML_source;
2008-08-14, by wenzelm
renamed P.ml_source to P.ML_source;
2008-08-14, by wenzelm
report doc_source;
2008-08-14, by wenzelm
added ML_source, doc_source;
2008-08-14, by wenzelm
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14, by wenzelm
added source_of';
2008-08-14, by wenzelm
P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-14, by wenzelm
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-14, by wenzelm
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
retrieve_thms: transfer fact position to result;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-14, by wenzelm
made SML/NJ happy;
2008-08-14, by wenzelm
removed obsolete present_html -- now part of regular theory presentation;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
ProofDisplay.add_hook;
2008-08-13, by wenzelm
simplified present_local_theory/proof;
2008-08-13, by wenzelm
ProofDisplay.theory_results;
2008-08-13, by wenzelm
removed obsolete present_results;
2008-08-13, by wenzelm
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
2008-08-13, by wenzelm
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-13, by wenzelm
simplified markup commands;
2008-08-13, by wenzelm
simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-13, by wenzelm
added untabify_content;
2008-08-13, by wenzelm
tuned;
2008-08-13, by wenzelm
removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-08-13, by wenzelm
tuned document;
2008-08-13, by wenzelm
removed obsolete theorems;
2008-08-13, by wenzelm
Changed proof of strong induction rule to avoid infinite loop
2008-08-13, by berghofe
token_kind_markup: complete coverage;
2008-08-12, by wenzelm
OuterSyntax.scan: pass position;
2008-08-12, by wenzelm
message: ignored if body empty;
2008-08-12, by wenzelm
load_thy: removed obsolete dir argument;
2008-08-12, by wenzelm
abstract type span, tuned interfaces;
2008-08-12, by wenzelm
adapted ThyEdit operations;
2008-08-12, by wenzelm
added ignored, malformed transitions;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
Isabelle.command: inline former OuterSyntax.prepare_command;
2008-08-12, by wenzelm
load thy_edit.ML before outer_syntax.ML;
2008-08-12, by wenzelm
renamed unknown_span to malformed_span;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
updated generated file;
2008-08-12, by wenzelm
rudimentary code setup for set operations
2008-08-11, by haftmann
<applet>: more XHTML 1.0 Transitional conformance;
2008-08-11, by wenzelm
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11, by wenzelm
<pre>: removed xml:space, is already default;
2008-08-11, by wenzelm
produce XHTML 1.0 Transitional;
2008-08-11, by wenzelm
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-11, by wenzelm
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-11, by wenzelm
changed code setup
2008-08-11, by haftmann
re-arranged class dense_linear_order
2008-08-11, by haftmann
rudimentary code setup for set operations
2008-08-11, by haftmann
moved class wellorder to theory Orderings
2008-08-11, by haftmann
added parse_token (from proof_context.ML);
2008-08-10, by wenzelm
read_tyname/const/const_proper: report position;
2008-08-10, by wenzelm
pass position to get_fact;
2008-08-10, by wenzelm
pass token source to typ/term etc.;
2008-08-10, by wenzelm
added name property operation;
2008-08-10, by wenzelm
renamed ML_Lex.val_of to content_of;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
load args.ML later (after outer_parse.ML);
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
read_asts: report literal tokens;
2008-08-09, by wenzelm
tuned error message;
2008-08-09, by wenzelm
pos_of_token: Position.T;
2008-08-09, by wenzelm
dest: sort strings;
2008-08-09, by wenzelm
added literal;
2008-08-09, by wenzelm
read_token: more robust handling of empty text;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
tuned SymbolPos interface;
2008-08-09, by wenzelm
YXML.parse: allow text without markup, potentially empty;
2008-08-09, by wenzelm
added content;
2008-08-09, by wenzelm
added distance_of (permissive version);
2008-08-09, by wenzelm
count offset as well;
2008-08-08, by wenzelm
added offset/end_offset;
2008-08-08, by wenzelm
tuned formatting;
2008-08-08, by wenzelm
clean up dead code
2008-08-08, by krauss
made SML/NJ happy;
2008-08-08, by wenzelm
FundefLib.try_proof : attempt a proof and see if it works
2008-08-08, by krauss
added lemmas
2008-08-08, by nipkow
inner_syntax markup is back;
2008-08-07, by wenzelm
disabled inner_syntax markup for now;
2008-08-07, by wenzelm
added read_token -- with optional YXML encoding of position;
2008-08-07, by wenzelm
parse_token: use Syntax.read_token, pass full position information;
2008-08-07, by wenzelm
tuned;
2008-08-07, by wenzelm
map_default: more explicit scope;
2008-08-07, by wenzelm
datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07, by wenzelm
simplified Antiquote signature;
2008-08-07, by wenzelm
more precise positions due to SymbolsPos.implode_delim;
2008-08-07, by wenzelm
simplified Antiq: regular SymbolPos.text with position;
2008-08-07, by wenzelm
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
2008-08-07, by wenzelm
only increment column if valid;
2008-08-07, by wenzelm
install_pp Position.T;
2008-08-07, by wenzelm
Position.start;
2008-08-07, by wenzelm
SymbolPos.explode;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
Antiquote.read/read_arguments;
2008-08-07, by wenzelm
updated type of nested sources;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
adapted Scan.extend_lexicon/merge_lexicons;
2008-08-07, by wenzelm
renamed scan_antiquotes to read;
2008-08-07, by wenzelm
export not_eof;
2008-08-07, by wenzelm
reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-07, by wenzelm
advance: single argument (again);
2008-08-07, by wenzelm
Symbols with explicit position information.
2008-08-07, by wenzelm
added General/symbol_pos.ML;
2008-08-07, by wenzelm
Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06, by ballarin
added lemma
2008-08-06, by nipkow
made SML/NJ happy;
2008-08-06, by wenzelm
Reverted last change, since it caused incompatibilities.
2008-08-06, by berghofe
fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06, by wenzelm
T.end_position_of;
2008-08-06, by wenzelm
adapted Antiq;
2008-08-06, by wenzelm
parse_sort/typ/term/prop: report markup;
2008-08-06, by wenzelm
sort/typ/term/prop: inner_syntax markup encodes original source position;
2008-08-06, by wenzelm
removed obsolete range_of (already included in position);
2008-08-06, by wenzelm
report markup;
2008-08-06, by wenzelm
Antiq: inner vs. outer position;
2008-08-06, by wenzelm
of_properties: observe Markup.position_properties';
2008-08-06, by wenzelm
added position_properties';
2008-08-06, by wenzelm
token: maintain of source, which retains original position information;
2008-08-05, by wenzelm
moved OuterLex.count here;
2008-08-05, by wenzelm
improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05, by wenzelm
advance: operate on symbol list (less overhead);
2008-08-05, by wenzelm
added token;
2008-08-05, by wenzelm
fix HOL/ex/LexOrds.thy; add to regression
2008-08-05, by krauss
added report;
2008-08-05, by wenzelm
removed axiom;
2008-08-05, by wenzelm
get_fact: report position;
2008-08-05, by wenzelm
Facts.lookup: return static/dynamic status;
2008-08-05, by wenzelm
position scanner: encode token range;
2008-08-04, by wenzelm
added encode_range;
2008-08-04, by wenzelm
added end_line, end_column properties;
2008-08-04, by wenzelm
meta_subst: xsymbols make it work with clean Pure;
2008-08-04, by wenzelm
abstract type Scan.stopper, position taken from last input token;
2008-08-04, by wenzelm
abstract type Scan.stopper;
2008-08-04, by wenzelm
abstract type stopper, may depend on final input;
2008-08-04, by wenzelm
removed obsolete apply_theorems(_i);
2008-08-04, by wenzelm
tuned signature;
2008-08-04, by wenzelm
removed obsolete note_thms_cmd;
2008-08-04, by wenzelm
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
2008-08-04, by wenzelm
tuned description;
2008-08-04, by wenzelm
replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
2008-08-04, by wenzelm
Quoted terms in consts_code declarations are now preprocessed as well.
2008-08-04, by berghofe
Exported eval_wrapper.
2008-08-04, by berghofe
- corrected bogus comment for function inst_conj_all
2008-08-04, by berghofe
removed dead code
2008-08-04, by krauss
simplified prepare_command;
2008-08-04, by wenzelm
Isar.command: explicitly set transaction position, as required for prepare_command errors;
2008-08-04, by wenzelm
Updated locale tests.
2008-08-04, by ballarin
Generalised polynomial lemmas from cring to ring.
2008-08-01, by ballarin
Removed import and lparams from locale record.
2008-08-01, by ballarin
made setsum executable on int.
2008-08-01, by nipkow
Tuned (for the sake of a meaningless log entry).
2008-07-31, by ballarin
New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-30, by ballarin
added hint about writing "x : set xs".
2008-07-30, by nipkow
simple lifters
2008-07-30, by haftmann
dropped imperative monad bind
2008-07-30, by haftmann
facts_of
2008-07-30, by haftmann
improved morphism
2008-07-30, by haftmann
SML_imp, OCaml_imp
2008-07-30, by haftmann
clarified
2008-07-30, by haftmann
tuned
2008-07-30, by haftmann
Zorn's Lemma for partial orders.
2008-07-29, by ballarin
Definitions and some lemmas for reflexive orderings.
2008-07-29, by ballarin
Lemmas added
2008-07-29, by ballarin
New theory on divisibility.
2008-07-29, by ballarin
Renamed theorems;
2008-07-29, by ballarin
New theorems on summation.
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp].
2008-07-29, by ballarin
New theory on divisibility;
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp];
2008-07-29, by ballarin
Haskell now living in the RealWorld
2008-07-29, by haftmann
corrected Pure dependency
2008-07-29, by haftmann
added removeAll
2008-07-29, by nipkow
tuned; explicit export of element accessors
2008-07-29, by haftmann
PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-29, by haftmann
some steps towards explicit class target for canonical interpretation
2008-07-29, by haftmann
declare
2008-07-29, by haftmann
*** empty log message ***
2008-07-28, by nipkow
simplified a proof
2008-07-27, by urbanc
tuned function name
2008-07-26, by haftmann
tuned bootstrap order
2008-07-26, by haftmann
subclass now also works for subclasses with empty specificaton
2008-07-25, by haftmann
dropped PureThy.note; added PureThy.add_thm
2008-07-25, by haftmann
added class preorder
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
added explicit root theory; some tuning
2008-07-25, by haftmann
tuned
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
added explicit purge_data
2008-07-21, by haftmann
added code generation
2008-07-21, by haftmann
fixed code generator setup
2008-07-21, by haftmann
(adjusted)
2008-07-21, by haftmann
Tuned and corrected ideal_tac for algebra.
2008-07-21, by chaieb
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
2008-07-21, by chaieb
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
2008-07-21, by chaieb
Tuned and simplified proofs
2008-07-21, by chaieb
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
2008-07-21, by chaieb
Relevant rules added to algebra's context
2008-07-21, by chaieb
renamed item to span, renamed contructors;
2008-07-20, by wenzelm
adapted ThyEdit.span;
2008-07-20, by wenzelm
maintain token range;
2008-07-20, by wenzelm
tty loop: do not report status;
2008-07-20, by wenzelm
added type range;
2008-07-20, by wenzelm
renamed command span markup;
2008-07-20, by wenzelm
SideKickParsedData: minimal content;
2008-07-20, by wenzelm
(adjusted)
2008-07-20, by haftmann
(adjusted)
2008-07-20, by haftmann
added verification framework for the HeapMonad and quicksort as example for this framework
2008-07-19, by bulwahn
build jedit plugin only if jedit is available;
2008-07-19, by wenzelm
misc tuning;
2008-07-18, by wenzelm
more class instantiations
2008-07-18, by haftmann
refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-18, by haftmann
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-18, by haftmann
fixed Scala path;
2008-07-18, by wenzelm
tuned build order;
2008-07-17, by wenzelm
proper purge_tmp;
2008-07-17, by wenzelm
tuned message;
2008-07-17, by wenzelm
tuned line breaks (NB: generated text is inserted here);
2008-07-17, by wenzelm
proper usage message;
2008-07-17, by wenzelm
make Isabelle source distribution (via Mercurial);
2008-07-17, by wenzelm
explicit Distribution.changelog;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
ThyInfo.remove_thy;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
use ../isabelle.sty and ../isabellesym.sty;
2008-07-17, by wenzelm
tuned whitespace;
2008-07-17, by wenzelm
removed old checklist;
2008-07-17, by wenzelm
obsolete;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
discontinued maketags;
2008-07-17, by wenzelm
assume GNU tar and find;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
use ../isabellesym.sty, which is always available;
2008-07-17, by wenzelm
Admin/build browser;
2008-07-17, by wenzelm
less verbosity;
2008-07-17, by wenzelm
Administrative build -- finish Isabelle source distribution.
2008-07-17, by wenzelm
simplified proofs
2008-07-17, by krauss
beautified proofs
2008-07-17, by nipkow
added lemmas
2008-07-17, by nipkow
Added Standardization theory to nominal examples.
2008-07-16, by berghofe
Added Standardization theory.
2008-07-16, by berghofe
editor model: run interactively for now;
2008-07-16, by wenzelm
updated generated file;
2008-07-16, by wenzelm
identify: more informative id in Toplevel.debug mode;
2008-07-16, by wenzelm
shortlogentry/filelogentry: show shortdate and full description;
2008-07-16, by wenzelm
Removed uses of context element includes.
2008-07-16, by ballarin
added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-16, by wenzelm
export type id with no_id and create_command;
2008-07-16, by wenzelm
tuned;
2008-07-15, by wenzelm
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-15, by wenzelm
load thy_edit.ML before isar.ML;
2008-07-15, by wenzelm
modernized specifications and proofs;
2008-07-15, by wenzelm
Removed uses of context element includes.
2008-07-15, by ballarin
tuned
2008-07-15, by haftmann
tuned code theorem bookkeeping
2008-07-15, by haftmann
tuned changelogentry;
2008-07-15, by wenzelm
refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15, by wenzelm
support for command status;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
tuned;
2008-07-15, by wenzelm
simplified commit_exit;
2008-07-15, by wenzelm
simplified commit_exit: operate on previous node of final state, include warning here;
2008-07-15, by wenzelm
removed obsolete commit_exit;
2008-07-15, by wenzelm
added command 'linear_undo';
2008-07-15, by wenzelm
removed command 'redo';
2008-07-15, by wenzelm
adapted ThyInfo.end_theory;
2008-07-15, by wenzelm
dropped map; fixed swap
2008-07-15, by haftmann
curried gcd
2008-07-15, by haftmann
cover macbroy as well;
2008-07-14, by wenzelm
tuned filelogentry;
2008-07-14, by wenzelm
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14, by wenzelm
tuned message;
2008-07-14, by wenzelm
updated generated file;
2008-07-14, by wenzelm
inform_file_processed: Isar.init_point last!
2008-07-14, by wenzelm
removed HOL-Complex, which has been discontinued after Isabelle2008;
2008-07-14, by wenzelm
added HOL-Nominal image;
2008-07-14, by wenzelm
removed obsolete Pure/General/history.ML;
2008-07-14, by wenzelm
inform_file_processed: try harder not to fail, ensure
2008-07-14, by wenzelm
commit_exit: proper error;
2008-07-14, by wenzelm
export EXCURSION_FAIL;
2008-07-14, by wenzelm
dropped junk
2008-07-14, by haftmann
moved bootstrap of simplifier
2008-07-14, by haftmann
tuned
2008-07-14, by haftmann
end_theory: no result;
2008-07-14, by wenzelm
removed obsolete Toplevel.RESTART;
2008-07-14, by wenzelm
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
adapted IsarCmd.init_theory;
2008-07-14, by wenzelm
renamed theory to init_theory, removed obsolete kill argument;
2008-07-14, by wenzelm
added commit_exit;
2008-07-14, by wenzelm
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-07-14, by krauss
renamed conversions to _conv, tuned
2008-07-14, by krauss
Simplified proofs
2008-07-14, by chaieb
Simple theorems about zgcd moved to GCD.thy
2008-07-14, by chaieb
Theorem names as in IntPrimes.thy, also several theorems moved from there
2008-07-14, by chaieb
Fixed proofs.
2008-07-14, by chaieb
ProofNode.current
2008-07-14, by wenzelm
command 'redo' no longer available;
2008-07-14, by wenzelm
replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-14, by wenzelm
removed obsolete 'redo' command;
2008-07-14, by wenzelm
removed obsolete history commands;
2008-07-14, by wenzelm
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
2008-07-14, by wenzelm
obsolete (cf. proof_node.ML);
2008-07-14, by wenzelm
removed Isar/proof_history.ML;
2008-07-14, by wenzelm
added further simple interfaces
2008-07-14, by haftmann
simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-14, by haftmann
unified curried gcd, lcm, zgcd, zlcm
2008-07-14, by haftmann
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
instance real_field < field_char_0;
2008-07-11, by huffman
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-11, by haftmann
Fract now total; improved code generator setup
2008-07-11, by haftmann
simple inheritance concept
2008-07-11, by haftmann
tuned thyname lookup
2008-07-11, by haftmann
fixed layout
2008-07-11, by haftmann
explicit completions of arities
2008-07-11, by haftmann
tuned order
2008-07-11, by haftmann
antiquotation
2008-07-11, by haftmann
improved code generator setup
2008-07-11, by haftmann
explicit dependency
2008-07-11, by haftmann
class instead of axclass
2008-07-11, by haftmann
tuned import
2008-07-11, by haftmann
separate class dvd for divisibility predicate
2008-07-11, by haftmann
temporarily disable at-sml-dev-p
2008-07-11, by kleing
updated generated file;
2008-07-10, by wenzelm
restart: Isar.init_point;
2008-07-10, by wenzelm
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
2008-07-10, by wenzelm
activated new versions of undo, kill_proof;
2008-07-10, by wenzelm
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
2008-07-10, by wenzelm
added print;
2008-07-10, by wenzelm
added ProofGeneral.isar_kill_proof;
2008-07-10, by wenzelm
added Isar.init_point, Isar.kill;
2008-07-10, by wenzelm
export init_point;
2008-07-10, by wenzelm
added Isar.linear_undo;
2008-07-10, by wenzelm
tuned;
2008-07-10, by wenzelm
tty interaction: do not move point after error;
2008-07-10, by wenzelm
change_lexicons: no verbosity;
2008-07-10, by wenzelm
added Isar.undo, which emulates old-style undo on global tty state;
2008-07-10, by wenzelm
provide old-style undo operation (still unused);
2008-07-10, by wenzelm
added prompt markup;
2008-07-10, by wenzelm
@{lemma}: allow terminal method;
2008-07-10, by wenzelm
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-07-10, by wenzelm
added is_diag;
2008-07-10, by wenzelm
slightly improved @{lemma} (both for latex and ML);
2008-07-10, by wenzelm
misc tuning;
2008-07-10, by wenzelm
Fixed (harmless) typo in closing *}.
2008-07-10, by ballarin
by intro_locales -> ..
2008-07-10, by huffman
instance real_field < field_char_0
2008-07-10, by huffman
remove redundant lemmas about cmod
2008-07-09, by huffman
removed owner;
2008-07-09, by wenzelm
tuned description;
2008-07-09, by wenzelm
changes wrt. gitweb style;
2008-07-09, by wenzelm
style = isabelle (based on gitweb);
2008-07-09, by wenzelm
rearrange instantiations
2008-07-09, by huffman
added get_first;
2008-07-09, by wenzelm
updated generated file;
2008-07-08, by wenzelm
updated generated file;
2008-07-08, by wenzelm
fix more typos
2008-07-08, by huffman
fix another typo
2008-07-08, by huffman
fix typo
2008-07-08, by huffman
updated generated file;
2008-07-08, by wenzelm
global commands: explicit graph;
2008-07-08, by wenzelm
export str_of;
2008-07-08, by wenzelm
clarified code
2008-07-08, by haftmann
exported weaken combinator
2008-07-08, by haftmann
refined arity property concept
2008-07-08, by haftmann
fix: using IntInf.int for SML
2008-07-08, by haftmann
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
removed obsolete touch_child_thys;
2008-07-08, by wenzelm
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
more qualified ThyInfo names;
2008-07-08, by wenzelm
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
2008-07-08, by wenzelm
removed unused href_opt_name;
2008-07-08, by wenzelm
migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware
2008-07-08, by kleing
retired mac-sml-dev.
2008-07-07, by kleing
absolute imports of HOL/*.thy theories
2008-07-07, by haftmann
prefer theorem names without numbers
2008-07-04, by huffman
HOL-NSA
2008-07-04, by huffman
added marginal setup for code generation
2008-07-04, by haftmann
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
2008-07-03, by huffman
removed old NSPrimes, cf. NSA/Examples/;
2008-07-03, by wenzelm
cvsps: back to non-verbose mode;
2008-07-03, by wenzelm
removed old Complex/ex/NSPrimes.thy;
2008-07-03, by wenzelm
maxfiles = 50;
2008-07-03, by wenzelm
more sessions;
2008-07-03, by wenzelm
more precise dependencies for HOL-Word and HOL-NSA;
2008-07-03, by wenzelm
fixed extremely slow proof of Chain_inits_DiffI
2008-07-03, by huffman
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
2008-07-03, by huffman
move proofs of add_left_cancel and add_right_cancel into the correct locale
2008-07-03, by huffman
cvsps -v (verbose);
2008-07-03, by wenzelm
removed nonstandard analysis theories to HOL-NSA
2008-07-03, by huffman
moved theories to HOL/NSA
2008-07-03, by huffman
add HOL-NSA
2008-07-03, by huffman
use patched cvsps to workaround loss of "foo: bar;" log entries;
2008-07-03, by wenzelm
move nonstandard analysis theories to NSA directory
2008-07-03, by huffman
back to default style, which shows files in changelog view;
2008-07-03, by wenzelm
added description;
2008-07-03, by wenzelm
tuned;
2008-07-03, by wenzelm
logrotate setup;
2008-07-03, by wenzelm
redirect stderr as well;
2008-07-03, by wenzelm
output to log file;
2008-07-03, by wenzelm
specific to CVS;
2008-07-03, by wenzelm
Isabelle repository service.
2008-07-03, by wenzelm
ensure hg/.hg/hgrc;
2008-07-03, by wenzelm
hgrc for conversion and web service;
2008-07-03, by wenzelm
provide HGRCPATH, taken from cvs/Admin;
2008-07-03, by wenzelm
code antiquotation roaring ahead
2008-07-03, by haftmann
tuned
2008-07-03, by haftmann
adjusted postprocessort setup
2008-07-03, by haftmann
added lemma antiquotation
2008-07-03, by haftmann
adjusted rep_datatype
2008-07-03, by haftmann
Adapted to changes in perm_simp / swap_simps.
2008-07-03, by berghofe
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
2008-07-03, by berghofe
Rewrote code to use swap_simps rather than calc_atm (which tends to
2008-07-03, by berghofe
moved HOL-Plain up;
2008-07-02, by wenzelm
rename Doc doc-src;
2008-07-02, by wenzelm
renamed Contents to Dirs to avoid case-conflict with doc/Contents;
2008-07-02, by wenzelm
section -> subsection
2008-07-02, by huffman
convert Isabelle CVS to Mercurial;
2008-07-02, by wenzelm
use begin and end for proofs in locales
2008-07-02, by huffman
exclude Distribution/bin/Isabelle;
2008-07-02, by wenzelm
init_theory: pass name explicitly;
2008-07-02, by wenzelm
replaced datatype category constructivism by is_theory/is_proof;
2008-07-02, by wenzelm
Toplevel.init_theory: pass name explicitly;
2008-07-02, by wenzelm
command: always keep transition, not just as initial status;
2008-07-02, by wenzelm
cached code for code antiquotation
2008-07-02, by haftmann
code antiquotation roaring ahead
2008-07-02, by haftmann
cleaned up some code generator configuration
2008-07-02, by haftmann
tuned;
2008-07-01, by wenzelm
added datatype category;
2008-07-01, by wenzelm
replaced datatype kind by OuterKeyword.category;
2008-07-01, by wenzelm
clean: HOL-Plain;
2008-07-01, by wenzelm
prove lemma finite in context of finite class
2008-07-01, by huffman
added HOL-Plain;
2008-07-01, by wenzelm
explicit identification of toplevel commands, with status etc.;
2008-07-01, by wenzelm
added name_of;
2008-07-01, by wenzelm
added get_id/put_id;
2008-07-01, by wenzelm
(removed Complex/ROOT.ML)
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
tuned
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
put file dependencies on separate lines
2008-07-01, by huffman
range_composition no longer in simp set
2008-07-01, by huffman
remove simp attribute from range_composition
2008-07-01, by huffman
rename INF to INFM
2008-07-01, by huffman
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
2008-07-01, by huffman
remove redundant instance proof finite_po < cpo
2008-07-01, by huffman
remove unused lemma is_lub_Iup'
2008-07-01, by huffman
replace lub (range Y) with (LUB i. Y i)
2008-07-01, by huffman
add file dependencies
2008-07-01, by huffman
universal bifinite domain
2008-07-01, by huffman
isomorphisms between naturals and sums, products, and finite sets
2008-07-01, by huffman
theory of algebraic deflations
2008-07-01, by huffman
theory of eventually-constant sequences
2008-07-01, by huffman
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-07-01, by huffman
rename compact_approx to compact_take
2008-07-01, by huffman
less
more
|
(0)
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip