# HG changeset patch
# User wenzelm
# Date 1447422570 -3600
# Node ID cfabbc0839777547c103a99fa9ff658b6111e67b
# Parent  f217bbe4e93e5cd2e84e39713c0719516833c8a2
more uniform jEdit properties;

diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Eisbach/Base.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Eisbach/Manual.thy
--- 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"
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Eisbach/Preface.thy
--- 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"
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Base.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Eq.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Integration.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Isar.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Local_Theory.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Logic.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/ML.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Prelim.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Proof.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Syntax.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Implementation/Tactic.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Base.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/First_Order_Logic.thy
--- 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>
 
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Framework.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Generic.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Preface.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Proof.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Proof_Script.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Quick_Reference.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Spec.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Symbols.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/Isar_Ref/Synopsis.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/JEdit/Base.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/JEdit/JEdit.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Base.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Basics.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Misc.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Presentation.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Scala.thy
--- 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
diff -r f217bbe4e93e -r cfabbc083977 src/Doc/System/Sessions.thy
--- 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