| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
7f9cbadc |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned context specifications and proofs;
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
5f9d11da |
|
05-Jun-2006 |
krauss <none@none> |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.
|
| #
bf8f2b17 |
|
22-Mar-2005 |
paulson <none@none> |
tidied
|
| #
681aa5e4 |
|
05-Feb-2003 |
paulson <none@none> |
more tidying
|
| #
4f0c87b6 |
|
24-Jan-2003 |
paulson <none@none> |
Partial conversion of UNITY to Isar new-style theories
|
| #
35842404 |
|
05-Mar-2001 |
paulson <none@none> |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|