Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+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.
maintain group in lthy data, implicit use in operations;
20080225, by wenzelm
tuned;
20080225, by wenzelm
LocalTheory.set_group for user command;
20080225, by wenzelm
inductive package: simplified group handling;
20080225, by wenzelm
Added dependency of Library on Pocklington.thy
20080225, by chaieb
Pocklington's Primality criterion
20080225, by chaieb
More primality theorems
20080225, by chaieb
A library for univariate polynomials  generalizes old Hyperreal/Poly.thy from reals to locales
20080225, by chaieb
A proof a the fundamental theorem of algebra
20080225, by chaieb
Uses Univ_Poly.thy
20080225, by chaieb
Does not import Poly anymore
20080225, by chaieb
Includes the derivates of polynomials  reals specific content of Poly
20080225, by chaieb
Two simple theorems about cmod moved to Complex.thy
20080225, by chaieb
Now imports Funamental_Theorem_Algebra
20080225, by chaieb
Added trivial theorems aboud cmod
20080225, by chaieb
Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
20080225, by chaieb
removed dead code; some cleanup
20080222, by krauss
nonoperative code antiquotation
20080222, by haftmann
nonoperative code antiquotation
20080222, by haftmann
added further interface for reading constants
20080222, by haftmann
added first version of datatype antiquotation
20080222, by haftmann
moved refute_tac to linarith.ML
20080222, by haftmann
more elaborate structure Distribution (filledin by makedist);
20080221, by wenzelm
keep ChangeLog.gz within distribution;
20080221, by wenzelm
removed junk;
20080221, by wenzelm
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas
20080221, by nipkow
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
20080221, by nipkow
removed NBE;
20080220, by wenzelm
removed ex/NBE.thy;
20080220, by wenzelm
fix proofs involving ile_def
20080220, by huffman
tuned structures in arith_data.ML
20080220, by haftmann
using only an relation predicate to construct div and mod
20080220, by haftmann
now in AFP
20080220, by nipkow
added system_out (back to multithreaded version  still suffers from noninterruptible wait in Poly/ML 5.1);
20080219, by wenzelm
removed General/system_process.ML (back to multithreaded version);
20080219, by wenzelm
replaced setpgrp by more elaborate setsid;
20080219, by wenzelm
slightly tuned
20080219, by urbanc
Yet another proof of False, this time using the strong case analysis rule.
20080219, by berghofe
tuned
20080218, by haftmann
system.pl  invoke shell command line (with robust signal handling);
20080218, by wenzelm
updated
20080218, by urbanc
added eqvtflag to subseteqlemma
20080218, by urbanc
proved linorder and wellorder class instances
20080218, by huffman
added get_parent (for AWE);
20080217, by wenzelm
added perl wrapper for robust signal handling;
20080217, by wenzelm
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
20080217, by huffman
removed spurious PolyML.makestring;
20080216, by wenzelm
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
20080216, by wenzelm
removed managed_process (cf. General/shell_process.ML);
20080216, by wenzelm
removed managed_process (cf. General/shell_process.ML);
20080216, by wenzelm
exn_message: added TimeLimit.TimeOut;
20080216, by wenzelm
export deny_secure;
20080216, by wenzelm
setmp: uninterruptible;
20080216, by wenzelm
System shell processes, with static input/output and propagation of interrupts.
20080216, by wenzelm
added General/system_process.ML;
20080216, by wenzelm
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
20080216, by huffman
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
20080216, by huffman
support for managed external processes;
20080215, by wenzelm
more lemmas
20080215, by nipkow
<= and < on nat no longer depend on wellfounded relations
20080215, by haftmann
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip