| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
9b4853bb |
|
23-Apr-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
f796bee5 |
|
19-Sep-2006 |
wenzelm <none@none> |
removed duplicate arities;
|
| #
3a22d7a5 |
|
03-Jan-2006 |
paulson <none@none> |
added explicit paths to required theories
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
737fdea6 |
|
02-Jun-2005 |
paulson <none@none> |
renamed "constrains" to "safety" to avoid keyword clash
|
| #
27f35147 |
|
08-Jul-2003 |
paulson <none@none> |
~= to neq
|
| #
dcb52ddf |
|
02-Jul-2003 |
paulson <none@none> |
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
|
| #
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
| #
b4eac3e6 |
|
29-Jan-2003 |
paulson <none@none> |
converted more UNITY theories to new-style
|
| #
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
| #
fb4bd978 |
|
22-Oct-2001 |
paulson <none@none> |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
to their abstract counterparts, while other binary numerals work correctly.
|
| #
6ddaa347 |
|
05-Oct-2001 |
wenzelm <none@none> |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
|
| #
64484fd5 |
|
05-Mar-2001 |
paulson <none@none> |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|