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 JavaScript-enabled browsers.
a bit of conversion to structured proofs
2002-05-07, by nipkow
*** empty log message ***
2002-05-07, by nipkow
be liberal about missing types;
2002-05-07, by wenzelm
*** empty log message ***
2002-05-07, by nipkow
tuned;
2002-05-07, by wenzelm
tuned presentation;
2002-05-07, by wenzelm
\documentclass{report};
2002-05-07, by wenzelm
use eq_thm_prop instead of slightly inadequate eq_thm;
2002-05-07, by wenzelm
clarified eq_thm;
2002-05-07, by wenzelm
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
2002-05-06, by nipkow
Added skeletons to speed up rewriting on proof terms.
2002-05-04, by berghofe
tuned
2002-04-30, by kleing
physical location of isabelle repository is now sunbroy2
2002-04-30, by kleing
added abstract;corrected RG_Basic Hoare rule.
2002-04-29, by prensani
Better compiler proof
2002-04-29, by nipkow
Had to update proof for some strange reason
2002-04-29, by nipkow
added rev_take and rev_drop
2002-04-29, by nipkow
New machine architecture and other direction of compiler proof.
2002-04-26, by nipkow
added "m <= n ==> m-n = 0" [simp]
2002-04-25, by nipkow
code generator: wfrec combinator is now implemented by ML function wf_rec.
2002-04-19, by berghofe
Added example for code generation.
2002-04-19, by berghofe
wf is no longer implemented by true (due to change in definition of class_rec).
2002-04-19, by berghofe
Improved definition of class_rec: no longer mixes algorithm and
2002-04-19, by berghofe
Added proof of Newman's lemma.
2002-04-19, by berghofe
new link to munich group
2002-04-16, by kleing
inserted tutorial
2002-04-16, by kleing
*** empty log message ***
2002-04-16, by nipkow
converted theory ex/Limit to Isar script, but it still needs work!
2002-04-15, by paulson
converted these theories to Isar format
2002-04-15, by paulson
*** empty log message ***
2002-04-12, by nipkow
*** empty log message ***
2002-04-08, by nipkow
*** empty log message ***
2002-04-08, by nipkow
tuned
2002-04-04, by kleing
conversion of Induct/{Slist,Sexp} to Isar scripts
2002-04-04, by paulson
flattened, uses locales
2002-04-04, by kleing
tuned
2002-04-04, by kleing
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
2002-04-03, by oheimb
conversion of some HOL/Induct proof scripts to Isar
2002-04-02, by paulson
Started to convert to locales
2002-04-02, by nipkow
mk_const_id now checks for clashes with reserved ML identifiers.
2002-03-28, by berghofe
added lbv completeness
2002-03-27, by kleing
finished lbv completeness
2002-03-27, by kleing
merge mono
2002-03-26, by kleing
lub property of ++_f
2002-03-26, by kleing
+_f is associative and commutative
2002-03-26, by kleing
tuned
2002-03-24, by kleing
cleanup + simpler monotonicity
2002-03-24, by kleing
more about match_exception_table
2002-03-24, by kleing
first steps in semilattices..
2002-03-21, by kleing
new_Addr defined in terms of J/State.new_Addr (for compiler)
2002-03-21, by kleing
small refactoring for lbv with semilattices
2002-03-20, by kleing
Fewer premises for restrict_image
2002-03-18, by paulson
cambridge
2002-03-14, by paulson
removed ex/set.ML
2002-03-14, by paulson
converted theory "set" to Isar and added some SET-VAR examples
2002-03-14, by paulson
increased treshold for "this expression could be extremely ambigous" warning
2002-03-14, by kleing
workaround for "ins" bug in sml/nj + code generator
2002-03-12, by kleing
*** empty log message ***
2002-03-12, by nipkow
added Berhard Rumpe, Farhad Mehta;
2002-03-11, by wenzelm
tuned;
2002-03-10, by wenzelm
canonical start state
2002-03-09, by kleing
in wellformed programs, exceptions are classes
2002-03-09, by kleing
tuned;
2002-03-08, by wenzelm
tuned;
Isabelle2002
2002-03-08, by wenzelm
tuned;
2002-03-08, by wenzelm
tuned;
2002-03-08, by wenzelm
removed Stanford mirror;
2002-03-08, by wenzelm
drop Stanford mirror;
2002-03-08, by wenzelm
for rail v 1.2
2002-03-08, by paulson
renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-03-07, by wenzelm
tuned;
2002-03-07, by wenzelm
*** empty log message ***
2002-03-07, by wenzelm
tuned;
2002-03-07, by wenzelm
tuned;
2002-03-07, by wenzelm
- made modes_of more robust
2002-03-07, by berghofe
val stdErr = std_out (std_err is unavaliable in polyml-3.x);
2002-03-06, by wenzelm
tuned;
2002-03-06, by wenzelm
tuned;
2002-03-06, by wenzelm
tuned;
2002-03-06, by wenzelm
added session_graph;
2002-03-06, by wenzelm
added two_is_prime;
2002-03-06, by wenzelm
tuned;
2002-03-06, by wenzelm
moved to Hyperreal-ex;
2002-03-06, by wenzelm
added HOL-Hyperreal-ex;
2002-03-06, by wenzelm
tuned;
2002-03-06, by wenzelm
some more stuff;
2002-03-06, by wenzelm
iff: conditional rules declared as ``unsafe'';
2002-03-05, by wenzelm
tuned;
2002-03-05, by wenzelm
more stuff;
2002-03-05, by wenzelm
Added two paragraphs on "rules" method and code generator.
2002-03-05, by berghofe
New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
2002-03-05, by prensani
Adding root.tex for HoareParallel
2002-03-05, by prensani
HoareParallel Theories
2002-03-05, by prensani
Target HoareParallel in IsaMakefile
2002-03-05, by prensani
isatool usedir -D generated Foo && isatool document Foo/generated;
2002-03-04, by wenzelm
'using' primitive;
2002-03-04, by wenzelm
tuned;
2002-03-04, by wenzelm
tuned;
2002-03-04, by wenzelm
records from logics-HOL;
2002-03-04, by wenzelm
improved ``deriving rules'';
2002-03-04, by wenzelm
hide SVC stuff (outdated);
2002-03-04, by wenzelm
\SHOWS;
2002-03-04, by wenzelm
tuned;
2002-03-04, by wenzelm
Tuned some references to LNCS volumes.
2002-03-04, by berghofe
Added some examples to section on executable specifications.
2002-03-04, by berghofe
MicroJava news
2002-03-03, by kleing
symbolized
2002-03-03, by kleing
proper handling of interrupts;
2002-03-02, by wenzelm
temporarily disabled HoareParallel target;
2002-03-02, by wenzelm
clarified outer syntax;
2002-03-01, by wenzelm
option -S 180;
2002-03-01, by wenzelm
clarified -l option;
2002-03-01, by wenzelm
structure Typtab;
2002-03-01, by wenzelm
tuned;
2002-03-01, by wenzelm
tuned;
2002-03-01, by wenzelm
tuned;
2002-03-01, by wenzelm
Completed annonce of HoareParallel
2002-03-01, by prensani
tuned;
2002-03-01, by wenzelm
some addresses
2002-03-01, by paulson
lcp's try
2002-03-01, by paulson
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip