From 600836ec7faab8d14d6c628b250298445c08085f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 19 Mar 2020 21:04:47 +0800 Subject: [PATCH] word_lib: re-sync with AFP; fix broken document Also switched on document generation so we don't miss these in the future. Signed-off-by: Gerwin Klein --- lib/Word_Lib/Distinct_Prop.thy | 2 +- lib/Word_Lib/ROOT | 2 +- lib/Word_Lib/Word_Lemmas.thy | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/Word_Lib/Distinct_Prop.thy b/lib/Word_Lib/Distinct_Prop.thy index ec08d2381..faa7c12d2 100644 --- a/lib/Word_Lib/Distinct_Prop.thy +++ b/lib/Word_Lib/Distinct_Prop.thy @@ -4,7 +4,7 @@ * SPDX-License-Identifier: BSD-2-Clause *) -chapter "Distinct Proposition" +section "Distinct Proposition" theory Distinct_Prop (* part of non-AFP Word_Lib *) imports diff --git a/lib/Word_Lib/ROOT b/lib/Word_Lib/ROOT index b71aa14a7..6aaf1575b 100644 --- a/lib/Word_Lib/ROOT +++ b/lib/Word_Lib/ROOT @@ -7,7 +7,7 @@ chapter Lib session Word_Lib (lib) = "HOL-Word" + - options [timeout = 150] + options [timeout = 150, document=pdf] sessions "HOL-Library" "HOL-Eisbach" diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy index ec3bdb33f..88d1975b1 100644 --- a/lib/Word_Lib/Word_Lemmas.thy +++ b/lib/Word_Lib/Word_Lemmas.thy @@ -1612,7 +1612,7 @@ lemma ucast_less_ucast: apply simp done -\ \This weaker version was previously called ucast_less_ucast. We retain it to +\ \This weaker version was previously called @{text ucast_less_ucast}. We retain it to support existing proofs.\ lemmas ucast_less_ucast_weak = ucast_less_ucast[OF order.strict_implies_order]