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

merged
2009-01-15, by wenzelm
one more [code del] declaration
2009-01-14, by huffman
misc cleanup and simplification;
2009-01-15, by wenzelm
added run_command (from isar_document.ML);
2009-01-15, by wenzelm
added command_state markup;
2009-01-15, by wenzelm
tuned ASCII art;
2009-01-14, by wenzelm
declare pCons_0_0 [code post]
2009-01-13, by huffman
merged
2009-01-13, by huffman
code generation for polynomials
2009-01-13, by huffman
merged
2009-01-13, by wenzelm
more [code del] declarations
2009-01-13, by huffman
declare more definitions [code del]
2009-01-13, by huffman
define polynomial multiplication using poly_rec
2009-01-13, by huffman
merged.
2009-01-13, by huffman
declare smult rules [simp]
2009-01-13, by huffman
simplify proof of coeff_mult_degree_sum
2009-01-13, by huffman
convert Deriv.thy to use new Polynomial library (incomplete)
2009-01-13, by huffman
Integration imports ATP_Linkup (for metis)
2009-01-13, by huffman
misc internal rearrangements;
2009-01-13, by wenzelm
replaced sys_error by plain error;
2009-01-13, by wenzelm
merged
2009-01-13, by wenzelm
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
2009-01-12, by huffman
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
2009-01-12, by huffman
add Polynomial.thy to makefile
2009-01-12, by huffman
add lemmas poly_power, poly_roots_finite
2009-01-12, by huffman
declare dvd_minus_iff and minus_dvd_iff [iff]
2009-01-12, by huffman
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
2009-01-12, by huffman
added Isar/isar_document.ML: Interactive Isar documents.
2009-01-13, by wenzelm
export list;
2009-01-13, by wenzelm
correctness and uniqueness of synthetic division
2009-01-12, by huffman
add synthetic division algorithm for polynomials
2009-01-12, by huffman
add list-style syntax for pCons
2009-01-12, by huffman
add recursion combinator poly_rec; define poly function using poly_rec
2009-01-12, by huffman
add lemmas degree_{add,diff}_less
2009-01-12, by huffman
merged
2009-01-11, by wenzelm
new theory of polynomials
2009-01-11, by huffman
tuned categories;
2009-01-11, by wenzelm
added outer_keyword.scala: Isar command keyword classification;
2009-01-11, by wenzelm
added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-11, by wenzelm
load main entry points sequentially, for reduced memory demands;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by haftmann
explicit bookkeeping of intro rules and axiom
2009-01-11, by haftmann
stripped Id
2009-01-11, by haftmann
construct explicit class morphism
2009-01-11, by haftmann
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10, by wenzelm
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10, by wenzelm
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10, by wenzelm
remove_thy: perform PureThy.cancel_proofs;
2009-01-10, by wenzelm
added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10, by wenzelm
added pending_groups -- accumulates task groups of local derivations only;
2009-01-10, by wenzelm
added cancel_group;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10, by wenzelm
load_thy: explicit after_load phase for presentation;
2009-01-10, by wenzelm
excursion: commit_exit internally -- checkpoints are fully persistent now;
2009-01-10, by wenzelm
slightly more robust matching of session name;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
fixed proof involving dvd;
2009-01-10, by wenzelm
tuned;
2009-01-10, by wenzelm
added force_result;
2009-01-10, by wenzelm
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2009-01-10, by wenzelm
simplified join_proofs;
2009-01-10, by wenzelm
merged
2009-01-09, by wenzelm
added split_thy_path;
2009-01-09, by wenzelm
added running task markup;
2009-01-09, by wenzelm
tuned;
2009-01-08, by wenzelm
merged
2009-01-08, by wenzelm
merged
2009-01-09, by wenzelm
merged.
2009-01-09, by huffman
fix proof broken by changes in dvd theory
2009-01-09, by huffman
merged.
2009-01-08, by huffman
remove type-specific proofs
2009-01-08, by huffman
add lemma dvd_diff to class comm_ring_1
2009-01-08, by huffman
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
2009-01-08, by huffman
move lemmas mult_minus{left,right} inside class ring
2009-01-08, by huffman
clean up division_ring proofs
2009-01-08, by huffman
add class ring_div; generalize mod/diff/minus proofs for class ring_div
2009-01-08, by huffman
generalize zmod_zmod_cancel -> mod_mod_cancel
2009-01-08, by huffman
generalize some div/mod lemmas; remove type-specific proofs
2009-01-08, by huffman
add tracing for domain package proofs
2009-01-07, by huffman
rename abbreviation square -> power2, to match theorem names
2009-01-06, by huffman
merged
2009-01-09, by haftmann
split of Imperative_HOL theories from HOL-Library
2009-01-08, by haftmann
NEWS and CONTRIBUTORS
2009-01-08, by haftmann
dded code_thm antiquotation
2009-01-08, by haftmann
made SML/NJ happy
2009-01-08, by haftmann
merged
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
tuned siganture of locale.ML
2009-01-07, by haftmann
tuned signature; internal code reorganisation
2009-01-07, by haftmann
tuned signature; changed locale predicate name convention
2009-01-07, by haftmann
changed locale predicate name convention
2009-01-07, by haftmann
inductive: added fork_mono flag;
2009-01-07, by wenzelm
added fork_mono flag, which is usually enabled in batch-mode only;
2009-01-07, by wenzelm
Proof.global_future_terminal_proof;
2009-01-07, by wenzelm
Proof.global_future_proof;
2009-01-07, by wenzelm
future_proof: refined version covers local_future_proof and global_future_proof;
2009-01-07, by wenzelm
more robust propagation of errors through bulk jobs;
2009-01-07, by wenzelm
qed/after_qed: singleton result;
2009-01-07, by wenzelm
Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;
2009-01-07, by wenzelm
future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-07, by wenzelm
added local_theory';
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
proper local_theory after Class.class
2009-01-07, by haftmann
more parallel loading;
2009-01-06, by wenzelm
more parallel loading;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
merged.
2009-01-06, by huffman
make cont_proc handle eta-contracted terms
2009-01-06, by huffman
implement is_closed_term using Term.loose_bvar
2009-01-06, by huffman
use Thm.close_derivation instead of standard
2009-01-05, by huffman
tuned;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
renamed structure ParList to Par_List;
2009-01-06, by wenzelm
parallelized merge_data;
2009-01-06, by wenzelm