#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
#
7c503729 |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <*>;
|
#
c9f3da2d |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <->;
|
#
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
7f9cbadc |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned context specifications and proofs;
|
#
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
b97be2fb |
|
22-Nov-2010 |
hoelzl <none@none> |
Replace surj by abbreviation; remove surj_on.
|
#
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
#
179dc521 |
|
22-Oct-2009 |
nipkow <none@none> |
inv_onto -> inv_into
|
#
def242e4 |
|
17-Oct-2009 |
nipkow <none@none> |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
3c4494d5 |
|
15-Feb-2003 |
paulson <none@none> |
minor revisions
|
#
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
|
#
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
#
ced4250f |
|
23-Sep-2000 |
paulson <none@none> |
added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
|
#
ee8f28f8 |
|
24-May-2000 |
paulson <none@none> |
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
|
#
dc3bc48c |
|
13-Apr-2000 |
nipkow <none@none> |
Times -> <*> ** -> <*lex*>
|
#
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
|
#
c3c5e8fb |
|
11-Oct-1999 |
paulson <none@none> |
working shapshot with "projecting" and "extending"
|
#
648cebd2 |
|
21-Sep-1999 |
paulson <none@none> |
project_act no longer has a special case to allow identity actions
|
#
eaea0ec7 |
|
10-Sep-1999 |
paulson <none@none> |
working snapshot
|
#
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 <
|
#
80ee482f |
|
27-Aug-1999 |
paulson <none@none> |
use of bij, new theorems, etc.
|
#
0cfea4c2 |
|
25-Aug-1999 |
paulson <none@none> |
project constants
|
#
64242e1c |
|
21-May-1999 |
paulson <none@none> |
made definition more readable
|
#
99a72cdf |
|
03-Mar-1999 |
paulson <none@none> |
new theory of extending the state space
|