History log of /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/BNF_Cardinal_Arithmetic.thy
Revision Date Author Comments
# f5796e6d 14-Feb-2018 wenzelm <none@none>

more symbols;
# 7c503729 27-Dec-2015 wenzelm <none@none>

discontinued ASCII replacement syntax <*>;
# 1901affb 18-Jul-2015 wenzelm <none@none>

isabelle update_cartouches;
# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;
# 31710314 18-Mar-2014 traytel <none@none>

tuned proofs; removed duplicated facts
# 7252d152 02-Mar-2014 blanchet <none@none>

life without 'metis'
# 94bfc55c 02-Mar-2014 blanchet <none@none>

optimize cardinal bounds involving natLeq (omega)
# bbeeaf3d 28-Feb-2014 traytel <none@none>

load Metis a little later
# d149e4f0 20-Feb-2014 noschinl <none@none>

less flex-flex pairs
# 5fd16e81 20-Jan-2014 blanchet <none@none>

tuned comments
# 47096efc 20-Jan-2014 blanchet <none@none>

renamed '_FP' files to 'BNF_' files

--HG--
rename : src/HOL/Cardinal_Arithmetic_FP.thy => src/HOL/BNF_Cardinal_Arithmetic.thy
rename : src/HOL/Cardinal_Order_Relation_FP.thy => src/HOL/BNF_Cardinal_Order_Relation.thy
rename : src/HOL/Constructions_on_Wellorders_FP.thy => src/HOL/BNF_Constructions_on_Wellorders.thy
rename : src/HOL/Wellorder_Embedding_FP.thy => src/HOL/BNF_Wellorder_Embedding.thy
rename : src/HOL/Wellorder_Relation_FP.thy => src/HOL/BNF_Wellorder_Relation.thy