History log of /seL4-l4v-master/l4v/isabelle/src/HOL/UNITY/Simple/Lift.thy
Revision Date Author Comments
# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# ef344a77 25-May-2016 wenzelm <none@none>

isabelle update_cartouches -c -t;


# 35f7dccd 23-Feb-2016 nipkow <none@none>

more canonical names


# 7f9cbadc 13-Mar-2012 wenzelm <none@none>

tuned context specifications and proofs;


# 335fd006 10-Sep-2011 wenzelm <none@none>

misc tuning and clarification;


# deac04eb 22-Jul-2010 wenzelm <none@none>

updated some headers;


# a5f328ca 12-May-2010 wenzelm <none@none>

modernized specifications;


# 079cde2d 17-Oct-2009 wenzelm <none@none>

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;


# 737fdea6 02-Jun-2005 paulson <none@none>

renamed "constrains" to "safety" to avoid keyword clash


# 4cb77476 09-Feb-2004 paulson <none@none>

generic of_nat and of_int functions, and generalization of iszero
and neg


# 5bb51f23 08-Feb-2003 paulson <none@none>

converting HOL/UNITY to use unconditional fairness


# 681aa5e4 05-Feb-2003 paulson <none@none>

more tidying


# 4f0c87b6 24-Jan-2003 paulson <none@none>

Partial conversion of UNITY to Isar new-style theories


# 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;


# 35842404 05-Mar-2001 paulson <none@none>

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp