isabelle: Graph

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

Future.release_results;
2008-09-27, by wenzelm
more tracing;
2008-09-27, by wenzelm
Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-27, by wenzelm
promise: include check into future body, i.e. joined results are always valid;
2008-09-27, by wenzelm
proper transfer of theorems that involve classes being instantiated here;
2008-09-27, by wenzelm
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
2008-09-27, by wenzelm
eliminated polymorphic equality;
2008-09-26, by wenzelm
added subset operation;
2008-09-26, by wenzelm
Added fresh_star_const.
2008-09-26, by berghofe
Added some more theorems to NominalData.
2008-09-26, by berghofe
Added some more lemmas that are useful in proof of strong induction rule.
2008-09-26, by berghofe
removed obsolete name convention "func"
2008-09-26, by haftmann
fixed typo
2008-09-26, by haftmann
clarified function transformator interface
2008-09-26, by haftmann
op = vs. eq
2008-09-26, by haftmann
moved future_scheduler flag to skip_proof.ML;
2008-09-25, by wenzelm
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