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

adapted to localized interpretation of min/max-lattice
2009-07-25, by haftmann
SUBPROOF/Obtain.result: named params;
2009-07-26, by wenzelm
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
2009-07-26, by wenzelm
advanced retrofit, which allows new subgoals and variables;
2009-07-26, by wenzelm
Variable.focus: named parameters;
2009-07-26, by wenzelm
lambda/cabs/all: named variants;
2009-07-26, by wenzelm
Goal.finish: explicit context for printing;
2009-07-26, by wenzelm
fixed Method.Basic;
2009-07-25, by wenzelm
eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;
2009-07-25, by wenzelm
Method.Basic: no position;
2009-07-25, by wenzelm
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
2009-07-25, by wenzelm
dequeue_towards: need to try imm_preds as well;
2009-07-25, by wenzelm
internal session timing;
2009-07-25, by wenzelm
enqueue: maintain transitive closure, which simplifies dequeue_towards;
2009-07-25, by wenzelm
ML_Context.the_generic_context;
2009-07-25, by wenzelm
eliminated redundant Library.multiply;
2009-07-25, by wenzelm
renamed structure Display_Goal to Goal_Display;
2009-07-25, by wenzelm
tuned tracing;
2009-07-25, by wenzelm
added Multithreading.real_time;
2009-07-25, by wenzelm
simplified/unified Multithreading.tracing_time;
2009-07-25, by wenzelm
get_name: cover only PThm, not PAxm;
2009-07-24, by wenzelm
eliminated OldGoals.read_term;
2009-07-24, by wenzelm
more antiquotations instead of adhoc ML stuff;
2009-07-24, by wenzelm
ML_Context.the_local_context;
2009-07-24, by wenzelm
eliminated the_context;
2009-07-24, by wenzelm
do not open OldGoals;
2009-07-24, by wenzelm
renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-24, by wenzelm
renamed functor BlastFun to Blast, require explicit theory;
2009-07-24, by wenzelm
eliminated OldGoals.prove_goal;
2009-07-24, by wenzelm
explicit OldGoals;
2009-07-24, by wenzelm
structure OldGoals: no pervasive names;
2009-07-24, by wenzelm
renamed functor ProjectRuleFun to Project_Rule;
2009-07-24, by wenzelm
renamed functor InductFun to Induct;
2009-07-24, by wenzelm
tuned;
2009-07-24, by wenzelm
renamed Pure/tctical.ML to Pure/tactical.ML;
2009-07-24, by wenzelm
eliminated print_goals_without_context -- proper pretty printing;
2009-07-24, by wenzelm
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-24, by wenzelm
removed Formal_Power_Series_Examples (cf. adea7a729c7a);
2009-07-24, by wenzelm
make: keep going by default;
2009-07-24, by wenzelm
merged
2009-07-23, by chaieb
merged
2009-07-23, by chaieb
fixed proof --- fact_setprod removed for fact_altdef_nat
2009-07-23, by chaieb
merged
2009-07-23, by chaieb
Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
2009-07-23, by chaieb
More theorems about pochhammer
2009-07-23, by chaieb
Moved theorem binomial_symmetric from Formal_Power_Series to here
2009-07-15, by chaieb
Moved important theorems from FPS_Examples to FPS --- they are not
2009-07-15, by chaieb
removed obsolete ML proof tools;
2009-07-23, by wenzelm
more @{theory} antiquotations;
2009-07-23, by wenzelm
eliminated adhoc ML code;
2009-07-23, by wenzelm
misc modernization: proper method setup instead of adhoc ML proofs;
2009-07-23, by wenzelm
global_claset_of;
2009-07-23, by wenzelm
Proper context for simpset_of, claset_of, clasimpset_of.
2009-07-23, by wenzelm
local simpset_of;
2009-07-23, by wenzelm
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-23, by wenzelm
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-23, by wenzelm
merged
2009-07-23, by wenzelm
paramify_vars: Term_Subst.map_atypsT_same
2009-07-23, by wenzelm
clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-23, by wenzelm
use regular Display.string_of_thm_global;
2009-07-23, by wenzelm
tuned ML_OPTIONS;
2009-07-23, by wenzelm
fixed doc
2009-07-23, by haftmann
Purely functional type inference.
2009-07-23, by berghofe
merged
2009-07-22, by haftmann
moved complete_lattice &c. into separate theory
2009-07-22, by haftmann
merged
2009-07-22, by Christian Urban
tuned proofs and added some lemmas
2009-07-22, by Christian Urban
merged
2009-07-22, by haftmann
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-22, by haftmann
set intersection and union now named inter and union
2009-07-22, by haftmann
spurious proof failure
2009-07-22, by haftmann
original rail implementation by Michael Kerscher;
2009-07-22, by wenzelm
merged, resolving trivial conflict;
2009-07-22, by wenzelm
News
2009-07-22, by nipkow
explicit antiquotation
2009-07-22, by haftmann
merged
2009-07-21, by haftmann
merged
2009-07-21, by haftmann
obey captialized directory names convention
2009-07-21, by haftmann
dropped ancient flat_names option
2009-07-21, by haftmann
dropped ancient flat_names option
2009-07-21, by haftmann
integrated add_triv_classes into evaluation stack
2009-07-21, by haftmann
more accurate check of judgment type
2009-07-21, by haftmann
UNIV_code now named UNIV_apply
2009-07-21, by haftmann
attempt for more concise setup of non-etacontracting binders
2009-07-21, by haftmann
moved abstract algebra section to the end
2009-07-21, by haftmann
merged
2009-07-21, by haftmann
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
2009-07-21, by haftmann
merged
2009-07-21, by haftmann
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
2009-07-21, by haftmann
merged
2009-07-20, by haftmann
dropped add_registration interface in locale
2009-07-20, by haftmann
Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
2009-07-21, by nipkow
Tests for executability of "prime"
2009-07-21, by nipkow
less ambitious settings;
2009-07-22, by wenzelm
future_job: more robust Exn.capture outside thread attribute change;
2009-07-22, by wenzelm
shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
2009-07-22, by wenzelm
future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
2009-07-21, by wenzelm
maintain Future.worker_group as management data;
2009-07-21, by wenzelm
join_proofs: implicit exception;
2009-07-21, by wenzelm
simultaneous join_proofs;
2009-07-21, by wenzelm
map: subgroup of worker_group;
2009-07-21, by wenzelm
added worker_group;
2009-07-21, by wenzelm
support for nested groups -- cancellation is propagated to peers and subgroups;
2009-07-21, by wenzelm
added flatten/flatten_list -- supercedes internal plain_exns;
2009-07-21, by wenzelm
propagate exceptions within future groups;
2009-07-21, by wenzelm
less ambitious ML_OPTIONS;
2009-07-21, by wenzelm
disabled macbroy6 -- hardware repair;
2009-07-21, by wenzelm
tuned;
2009-07-21, by wenzelm
tuned tracing;
2009-07-21, by wenzelm
prefer simultaneous join -- for improved scheduling;
2009-07-21, by wenzelm
tuned dequeu_towards: try immediate tasks before expensive all_preds;
2009-07-21, by wenzelm
Display.pretty_thm now requires a proper context;
2009-07-21, by wenzelm
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-21, by wenzelm
moved ProofContext.pretty_thm to Display.pretty_thm etc.;
2009-07-21, by wenzelm
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-07-20, by wenzelm
removed obsolete CVS Ids;
2009-07-20, by wenzelm
merged
2009-07-20, by wenzelm
merged
2009-07-20, by haftmann
deftab: only process theorems on demand
2009-07-20, by haftmann
no SAME exceptions in uncritical code
2009-07-20, by krauss