Mercurial
Mercurial
>
repos
>
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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
moved Univ_Poly to Library
20090116, by haftmann
merged
20090116, by haftmann
tuned
20090116, by haftmann
added cert_read_declaration; more exports; tuned signature
20090116, by haftmann
merged
20090115, by wenzelm
command 'Isar.edit_document': actually invoke edit_document;
20090115, by wenzelm
merged
20090115, by haftmann
fixed error message spacing
20090115, by haftmann
tuned interpretation code
20090115, by haftmann
tuned
20090115, by haftmann
type constraints and sort intersection
20090115, by haftmann
dropped $Id$
20090115, by haftmann
decativate Toplevel.debug after reading
20090115, by haftmann
exported break reference
20090115, by Christian Urban
tuned;
20090115, by wenzelm
edit_document: proper edits/edit markup, including the document id;
20090115, by wenzelm
replaced command_state by edits/edit;
20090115, by wenzelm
removed junk;
20090115, by wenzelm
merged
20090115, by wenzelm
one more [code del] declaration
20090114, by huffman
misc cleanup and simplification;
20090115, by wenzelm
added run_command (from isar_document.ML);
20090115, by wenzelm
added command_state markup;
20090115, by wenzelm
tuned ASCII art;
20090114, by wenzelm
declare pCons_0_0 [code post]
20090113, by huffman
merged
20090113, by huffman
code generation for polynomials
20090113, by huffman
merged
20090113, by wenzelm
more [code del] declarations
20090113, by huffman
declare more definitions [code del]
20090113, by huffman
define polynomial multiplication using poly_rec
20090113, by huffman
merged.
20090113, by huffman
declare smult rules [simp]
20090113, by huffman
simplify proof of coeff_mult_degree_sum
20090113, by huffman
convert Deriv.thy to use new Polynomial library (incomplete)
20090113, by huffman
Integration imports ATP_Linkup (for metis)
20090113, by huffman
misc internal rearrangements;
20090113, by wenzelm
replaced sys_error by plain error;
20090113, by wenzelm
merged
20090113, by wenzelm
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
20090112, by huffman
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
20090112, by huffman
add Polynomial.thy to makefile
20090112, by huffman
add lemmas poly_power, poly_roots_finite
20090112, by huffman
declare dvd_minus_iff and minus_dvd_iff [iff]
20090112, by huffman
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
20090112, by huffman
added Isar/isar_document.ML: Interactive Isar documents.
20090113, by wenzelm
export list;
20090113, by wenzelm
correctness and uniqueness of synthetic division
20090112, by huffman
add synthetic division algorithm for polynomials
20090112, by huffman
add liststyle syntax for pCons
20090112, by huffman
add recursion combinator poly_rec; define poly function using poly_rec
20090112, by huffman
add lemmas degree_{add,diff}_less
20090112, by huffman
merged
20090111, by wenzelm
new theory of polynomials
20090111, by huffman
tuned categories;
20090111, by wenzelm
added outer_keyword.scala: Isar command keyword classification;
20090111, by wenzelm
added Goal.future_enabled abstraction  now also checks that this is already
20090111, by wenzelm
load main entry points sequentially, for reduced memory demands;
20090111, by wenzelm
merged
20090111, by wenzelm
merged
20090111, by wenzelm
less ambitious ML_OPTIONS;
20090111, by wenzelm
merged
20090111, by wenzelm
merged
20090111, by haftmann
explicit bookkeeping of intro rules and axiom
20090111, by haftmann
stripped Id
20090111, by haftmann
construct explicit class morphism
20090111, by haftmann
less ambitious ML_OPTIONS;
20090111, by wenzelm
schedule_futures: save memory for nonparallel proofs, by applying after_load as soon as possible here;
20090110, by wenzelm
future_result: avoid expensive norm_proof (consider usedir option Q false in lowmemory situations);
20090110, by wenzelm
added parallel_proofs flag (default true, cf. usedir option Q), which can be disabled in lowmemory situations;
20090110, by wenzelm
remove_thy: perform PureThy.cancel_proofs;
20090110, by wenzelm
added cancel_proofs, based on task groups of "entered" proofs;
20090110, by wenzelm
added pending_groups  accumulates task groups of local derivations only;
20090110, by wenzelm
added cancel_group;
20090110, by wenzelm
merged
20090110, by wenzelm
schedule_futures: tuned final consolidation, explicit after_load phase;
20090110, by wenzelm
load_thy: explicit after_load phase for presentation;
20090110, by wenzelm
excursion: commit_exit internally  checkpoints are fully persistent now;
20090110, by wenzelm
slightly more robust matching of session name;
20090110, by wenzelm
merged
20090110, by wenzelm
fixed proof involving dvd;
20090110, by wenzelm
tuned;
20090110, by wenzelm
added force_result;
20090110, by wenzelm
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
20090110, by wenzelm
simplified join_proofs;
20090110, by wenzelm
merged
20090109, by wenzelm
added split_thy_path;
20090109, by wenzelm
added running task markup;
20090109, by wenzelm
tuned;
20090108, by wenzelm
merged
20090108, by wenzelm
merged
20090109, by wenzelm
merged.
20090109, by huffman
fix proof broken by changes in dvd theory
20090109, by huffman
merged.
20090108, by huffman
remove typespecific proofs
20090108, by huffman
add lemma dvd_diff to class comm_ring_1
20090108, by huffman
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
20090108, by huffman
move lemmas mult_minus{left,right} inside class ring
20090108, by huffman
clean up division_ring proofs
20090108, by huffman
add class ring_div; generalize mod/diff/minus proofs for class ring_div
20090108, by huffman
generalize zmod_zmod_cancel > mod_mod_cancel
20090108, by huffman
generalize some div/mod lemmas; remove typespecific proofs
20090108, by huffman
add tracing for domain package proofs
20090107, by huffman
rename abbreviation square > power2, to match theorem names
20090106, by huffman
merged
20090109, by haftmann
split of Imperative_HOL theories from HOLLibrary
20090108, by haftmann
NEWS and CONTRIBUTORS
20090108, by haftmann
dded code_thm antiquotation
20090108, by haftmann
made SML/NJ happy
20090108, by haftmann
merged
20090107, by wenzelm
merged
20090107, by haftmann
tuned siganture of locale.ML
20090107, by haftmann
tuned signature; internal code reorganisation
20090107, by haftmann
tuned signature; changed locale predicate name convention
20090107, by haftmann
changed locale predicate name convention
20090107, by haftmann
inductive: added fork_mono flag;
20090107, by wenzelm
added fork_mono flag, which is usually enabled in batchmode only;
20090107, by wenzelm
Proof.global_future_terminal_proof;
20090107, by wenzelm
Proof.global_future_proof;
20090107, by wenzelm
future_proof: refined version covers local_future_proof and global_future_proof;
20090107, by wenzelm
less
more

(0)
10000
3000
1000
120
+120
+1000
+3000
+10000
+30000
tip