--- a/src/Doc/Eisbach/Base.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Eisbach/Base.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
section \<open>Basic setup that is not included in the document\<close>
theory Base
--- a/src/Doc/Eisbach/Manual.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Manual
imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
--- a/src/Doc/Eisbach/Preface.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Eisbach/Preface.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Preface
imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
--- a/src/Doc/Implementation/Base.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Base.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Base
imports Main
begin
--- a/src/Doc/Implementation/Eq.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Eq.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Eq
imports Base
begin
--- a/src/Doc/Implementation/Integration.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Integration.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Integration
imports Base
--- a/src/Doc/Implementation/Isar.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Isar
imports Base
begin
--- a/src/Doc/Implementation/Local_Theory.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Local_Theory
imports Base
begin
--- a/src/Doc/Implementation/Logic.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Logic.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Logic
imports Base
begin
--- a/src/Doc/Implementation/ML.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory "ML"
imports Base
--- a/src/Doc/Implementation/Prelim.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Prelim.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Prelim
imports Base
begin
--- a/src/Doc/Implementation/Proof.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Proof
imports Base
begin
--- a/src/Doc/Implementation/Syntax.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Syntax.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Syntax
imports Base
--- a/src/Doc/Implementation/Tactic.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Tactic
imports Base
begin
--- a/src/Doc/Isar_Ref/Base.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Base.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Base
imports Pure
begin
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Document_Preparation
imports Base Main
begin
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,4 @@
+(*:maxLineLen=78:*)
section \<open>Example: First-Order Logic\<close>
--- a/src/Doc/Isar_Ref/Framework.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Framework
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Generic.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Generic
imports Base Main
begin
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory HOL_Specific
imports
Base
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Inner_Syntax
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Outer_Syntax
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Preface.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Preface.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Preface
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Proof.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Proof
imports Base Main
begin
@@ -5,6 +7,7 @@
chapter \<open>Proofs \label{ch:proofs}\<close>
text \<open>
+
Proof commands perform transitions of Isar/VM machine
configurations, which are block-structured, consisting of a stack of
nodes with three main components: logical proof context, current
--- a/src/Doc/Isar_Ref/Proof_Script.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Proof_Script
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Quick_Reference.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Quick_Reference
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Spec.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Spec
imports Base Main "~~/src/Tools/Permanent_Interpretation"
begin
--- a/src/Doc/Isar_Ref/Symbols.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Symbols.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Symbols
imports Base Main
begin
--- a/src/Doc/Isar_Ref/Synopsis.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Synopsis
imports Base Main
begin
--- a/src/Doc/JEdit/Base.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/JEdit/Base.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Base
imports Main
begin
--- a/src/Doc/JEdit/JEdit.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory JEdit
imports Base
--- a/src/Doc/System/Base.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Base.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,3 +1,5 @@
+(*:maxLineLen=78:*)
+
theory Base
imports Pure
begin
--- a/src/Doc/System/Basics.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Basics.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Basics
imports Base
--- a/src/Doc/System/Misc.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Misc.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Misc
imports Base
--- a/src/Doc/System/Presentation.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Presentation.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Presentation
imports Base
--- a/src/Doc/System/Scala.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Scala.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Scala
imports Base
--- a/src/Doc/System/Sessions.thy Fri Nov 13 14:11:54 2015 +0100
+++ b/src/Doc/System/Sessions.thy Fri Nov 13 14:49:30 2015 +0100
@@ -1,4 +1,4 @@
-(*:wrap=hard:maxLineLen=78:*)
+(*:maxLineLen=78:*)
theory Sessions
imports Base