#
09859749 |
|
18-Nov-2018 |
haftmann <none@none> |
removed legacy input syntax
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
6337ab39 |
|
12-Nov-2011 |
wenzelm <none@none> |
tuned proofs;
|
#
335fd006 |
|
10-Sep-2011 |
wenzelm <none@none> |
misc tuning and clarification;
|
#
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;
|
#
a84018cb |
|
24-Jul-2008 |
haftmann <none@none> |
added class preorder
|
#
46a1ad78 |
|
01-Jul-2005 |
berghofe <none@none> |
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
402829d8 |
|
15-Jul-2003 |
paulson <none@none> |
tidying
|
#
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
|
#
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");
|
#
20030c6d |
|
02-Mar-2001 |
ehmety <none@none> |
*** empty log message ***
|
#
ced4250f |
|
23-Sep-2000 |
paulson <none@none> |
added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
|
#
31503020 |
|
14-Jul-2000 |
paulson <none@none> |
used bounded quantification in definition of guarantees and other minor adjustments
|
#
af066af4 |
|
08-Dec-1999 |
paulson <none@none> |
abolition of localTo: instead "guarantees" has local vars as extra argument
|
#
fc68c146 |
|
31-Aug-1999 |
paulson <none@none> |
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants
|