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 JavaScript-enabled browsers.
*** empty log message ***
2000-11-27, by nipkow
*** empty log message ***
2000-11-26, by nipkow
*** empty log message ***
2000-11-26, by nipkow
hide many names from Datatype_Universe.
2000-11-24, by nipkow
exception Interrupt = SML90.Interrupt;
2000-11-24, by wenzelm
added exception Interrupt for use in function Library/try
2000-11-24, by paulson
arith_tac: atomize;
2000-11-23, by wenzelm
standard: close_derivation;
2000-11-23, by wenzelm
* HOL: syntax or "abs";
2000-11-23, by wenzelm
*** empty log message ***
2000-11-23, by nipkow
tuned;
2000-11-22, by wenzelm
tuned;
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by nipkow
tag result with name reference to final binding (basically just a comment);
2000-11-21, by wenzelm
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-21, by wenzelm
replace \<dots>;
2000-11-21, by wenzelm
unsymbolize;
2000-11-21, by wenzelm
quote executable;
2000-11-21, by wenzelm
tuned;
2000-11-21, by wenzelm
;
2000-11-21, by bauerg
adjusted for BV changes (Ok -> OK)
2000-11-21, by kleing
thebibliography environment: replaced the Springer version by the standard one
2000-11-21, by paulson
alternative function definition;
2000-11-21, by bauerg
*** empty log message ***
2000-11-21, by nipkow
BCV integration (type system is semilattice)
2000-11-20, by kleing
BCV integration (first step)
2000-11-20, by kleing
export freeze_thaw_type;
2000-11-18, by wenzelm
improved messages;
2000-11-18, by wenzelm
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18, by wenzelm
axclass ordered_ring;
2000-11-18, by wenzelm
quot_cond_function: simplified, support conditional definition;
2000-11-18, by wenzelm
abs_eq_0: #0 instead of 0;
2000-11-18, by wenzelm
symbol syntax for "abs";
2000-11-18, by wenzelm
added axclass ordered_field;
2000-11-18, by wenzelm
check result: Envir.beta_norm;
2000-11-17, by wenzelm
Envir.beta_norm;
2000-11-17, by wenzelm
added beta_norm;
2000-11-17, by wenzelm
tuned;
2000-11-17, by wenzelm
removed quot_cond_function1, quot_function1;
2000-11-17, by wenzelm
UNIV_witness;
2000-11-17, by wenzelm
Ring_and_Field;
2000-11-17, by wenzelm
Library/Ring_and_Field.thy;
2000-11-17, by wenzelm
rings and fields;
2000-11-16, by bauerg
Proof.assert_forward;
2000-11-16, by wenzelm
added not_equiv_sym, not_equiv_trans1/2;
2000-11-16, by wenzelm
added abs_mult, abs_eq_0, square_nonzero;
2000-11-16, by wenzelm
ground terms section: new intro
2000-11-16, by paulson
CTT
2000-11-16, by paulson
separate rules for function/operation definitions;
2000-11-15, by wenzelm
renamed integ_le_less to int_le_less;
2000-11-15, by wenzelm
updated;
2000-11-15, by wenzelm
isabellebody: \par at begin/end;
2000-11-15, by wenzelm
auto update
2000-11-14, by paulson
first version of Advanced Inductive Defs section
2000-11-14, by paulson
x-symbol support for Pi, Sigma, -->, : (membership)
2000-11-14, by paulson
new Main.thy as in HOL, ZF
2000-11-14, by paulson
added read_terms, read_props (simulataneous type-inference);
2000-11-13, by wenzelm
tuned statement args;
2000-11-13, by wenzelm
tuned IsarThy.theorem_i;
2000-11-13, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip