# HG changeset patch
# User wenzelm
# Date 1537795903 -7200
# Node ID ba8104f79d7bd759f24a26715040d174f806d33d
# Parent  480d60d3c5ef67fec3f45395360bb60d01170c70
misc tuning and modernization;

diff -r 480d60d3c5ef -r ba8104f79d7b src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 24 15:20:21 2018 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 24 15:31:43 2018 +0200
@@ -427,7 +427,10 @@
 
 print_locale! trivial
 
-context trivial begin thm x.Q [where ?x = True] end
+context trivial
+begin
+thm x.Q [where ?x = True]
+end
 
 sublocale trivial < y: trivial Q Q
   by unfold_locales
@@ -752,7 +755,8 @@
 
 print_locale! lgrp
 
-context lgrp begin
+context lgrp
+begin
 
 text \<open>Equations stored in target\<close>
 
@@ -788,7 +792,8 @@
 lemmas true_copy = private.true
 end
 
-context container begin
+context container
+begin
 ML \<open>(Context.>> (fn generic => let val context = Context.proof_of generic
   val _ = Proof_Context.get_thms context "private.true" in generic end);
   raise Fail "thm private.true was persisted")
@@ -799,8 +804,8 @@
 
 section \<open>Interpretation in proofs\<close>
 
-lemma True
-proof
+notepad
+begin
   interpret "local": lgrp "(+)" "0" "minus"
     by unfold_locales  (* subsumed *)
   {
@@ -815,10 +820,10 @@
   then interpret local_free: lgrp "(+)" zero "minus" for zero
     by unfold_locales
   thm local_free.lone [where ?zero = 0]
-qed
+end
 
-lemma True
-proof
+notepad
+begin
   {
     fix pand and pnot and por
     assume passoc: "\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))"
@@ -835,6 +840,6 @@
     print_interps logic_o
     have "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
   }
-qed
+end
 
 end