| Sun, 22 Jun 2014 12:37:55 +0200 |
nipkow |
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
|
file |
diff |
annotate
|
| Sat, 21 Jun 2014 15:46:52 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 22:49:02 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 15:18:52 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:34 +0200 |
wenzelm |
removed duplicate arities;
|
file |
diff |
annotate
|
| Mon, 08 Nov 2004 16:53:50 +0100 |
paulson |
tidied comments
|
file |
diff |
annotate
|
| Fri, 15 Aug 2003 13:07:01 +0200 |
paulson |
A document for UNITY
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 12:56:48 +0200 |
paulson |
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 10:35:56 +0100 |
paulson |
converting more UNITY theories to new-style
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Mon, 05 Mar 2001 15:32:54 +0100 |
paulson |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|
file |
diff |
annotate
|