| #
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
7c503729 |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <*>;
|
| #
f55b23fd |
|
23-Jul-2015 |
wenzelm <none@none> |
more symbols by default, without xsymbols mode;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
| #
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
f20bcaa2 |
|
11-Jul-2003 |
oheimb <none@none> |
added upd_fst, upd_snd, some thms
|
| #
875e024b |
|
27-Feb-2003 |
paulson <none@none> |
restored some deleted lemmas
|
| #
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
| #
2380b71a |
|
04-Feb-2003 |
paulson <none@none> |
some x-symbols
|
| #
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
| #
e1895cc3 |
|
29-Jan-2003 |
paulson <none@none> |
converting UNITY to new-style theories
|
| #
71fec134 |
|
24-Jan-2003 |
paulson <none@none> |
More conversion of UNITY to Isar new-style theories
|
| #
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;
|
| #
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
| #
49598266 |
|
18-Feb-2000 |
paulson <none@none> |
New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.
|
| #
808483ad |
|
13-Jan-2000 |
paulson <none@none> |
working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.
|
| #
35a6290a |
|
30-Nov-1999 |
paulson <none@none> |
working version with new theory ELT
|
| #
9c72ed0f |
|
27-Oct-1999 |
paulson <none@none> |
working again; new treatment of LocalTo
|
| #
2a3c4b0b |
|
18-Oct-1999 |
paulson <none@none> |
exchanged the first two args of "project" and "drop_prog"
|
| #
2289e39b |
|
18-Oct-1999 |
paulson <none@none> |
working version with localTo[C] instead of localTo
|
| #
255920c7 |
|
04-Oct-1999 |
paulson <none@none> |
most results now refer to those for "extend"
|
| #
78a5f3f4 |
|
29-Sep-1999 |
paulson <none@none> |
working snapshot with new theory "Project"
|
| #
2d04f860 |
|
06-Sep-1999 |
paulson <none@none> |
working snapshot
|
| #
19656c80 |
|
31-Aug-1999 |
paulson <none@none> |
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
|
| #
c0632f8c |
|
06-Aug-1999 |
paulson <none@none> |
new theory UNITY/Lift_prog
|