# HG changeset patch
# User wenzelm
# Date 963481300 -7200
# Node ID bafe45732b106b4396ef50bd4ba0e1b2d1d9dcf6
# Parent  0d2b31e1ea1b910fa24191933f1b478a9476da88
tuned;

diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/Antiquote.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,35 +1,36 @@
 (*  Title:      HOL/ex/Antiquote.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Simple quote / antiquote example.
 *)
 
-theory Antiquote = Main:;
+theory Antiquote = Main:
 
 syntax
-  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999);
+  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
 
 constdefs
   var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
   "var x env == env x"
 
   Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
-  "Expr exp env == exp env";
+  "Expr exp env == exp env"
 
-parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *};
-print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *};
+parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
+print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
 
-term "EXPR (a + b + c)";
-term "EXPR (a + b + c + VAR x + VAR y + 1)";
-term "EXPR (VAR (f w) + VAR x)";
+term "EXPR (a + b + c)"
+term "EXPR (a + b + c + VAR x + VAR y + 1)"
+term "EXPR (VAR (f w) + VAR x)"
 
-term "Expr (%env. env x)";				(*improper*)
-term "Expr (%env. f env)";
-term "Expr (%env. f env + env x)";			(*improper*)
-term "Expr (%env. f env y z)";
-term "Expr (%env. f env + g y env)";
-term "Expr (%env. f env + g env y + h a env z)";
+term "Expr (%env. env x)"				(*improper*)
+term "Expr (%env. f env)"
+term "Expr (%env. f env + env x)"			(*improper*)
+term "Expr (%env. f env y z)"
+term "Expr (%env. f env + g y env)"
+term "Expr (%env. f env + g env y + h a env z)"
 
-end;
+end
 
diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/BinEx.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1998  University of Cambridge
 
 Definition of normal form for proving that binary arithmetic on
-ormalized operands yields normalized results.
+normalized operands yields normalized results.
 
 Normal means no leading 0s on positive numbers and no leading 1s on negatives.
 *)
diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/MonoidGroup.thy
--- a/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,33 +1,31 @@
 (*  Title:      HOL/ex/MonoidGroup.thy
     ID:         $Id$
     Author:     Markus Wenzel
-    Copyright   1996 TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Monoids and Groups as predicates over record schemes.
 *)
 
-MonoidGroup = HOL + Record +
-
+theory MonoidGroup = Main:
 
 record 'a monoid_sig =
   times :: "['a, 'a] => 'a"
   one :: 'a
 
-record 'a group_sig = 'a monoid_sig +
+record 'a group_sig = "'a monoid_sig" +
   inv :: "'a => 'a"
 
 constdefs
-  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) => bool"
+  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
   "monoid M == ALL x y z.
     times M (times M x y) z = times M x (times M y z) &
     times M (one M) x = x & times M x (one M) = x"
 
-  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
   "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
 
-  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
-    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
+    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
   "reverse M == M (| times := %x y. times M y x |)"
 
-
 end
diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/Multiquote.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,16 +1,17 @@
 (*  Title:      HOL/ex/Multiquote.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Multiple nested quotations and anti-quotations -- basically a
 generalized version of de-Bruijn representation.
 *)
 
-theory Multiquote = Main:;
+theory Multiquote = Main:
 
 syntax
   "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 1000);
+  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 1000)
 
 parse_translation {*
   let
@@ -28,18 +29,18 @@
     fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [("_quote", quote_tr)] end
-*};
+*}
 
-text {* basic examples *};
-term ".(a + b + c).";
-term ".(a + b + c + `x + `y + 1).";
-term ".(`(f w) + `x).";
-term ".(f `x `y z).";
+text {* basic examples *}
+term ".(a + b + c)."
+term ".(a + b + c + `x + `y + 1)."
+term ".(`(f w) + `x)."
+term ".(f `x `y z)."
 
-text {* advanced examples *};
-term ".(.(` `x + `y).).";
-term ".(.(` `x + `y). o `f).";
-term ".(`(f o `g)).";
-term ".(.( ` `(f o `g) ).).";
+text {* advanced examples *}
+term ".(.(` `x + `y).)."
+term ".(.(` `x + `y). o `f)."
+term ".(`(f o `g))."
+term ".(.( ` `(f o `g) ).)."
 
-end;
+end
diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/Points.thy
--- a/src/HOL/ex/Points.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/Points.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/ex/Points.thy
     ID:         $Id$
     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Points and coloured points --- using extensible records in HOL *}
diff -r 0d2b31e1ea1b -r bafe45732b10 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jul 13 11:41:40 2000 +0200
@@ -1,9 +1,7 @@
 (*  Title:      HOL/ex/ROOT.ML
     ID:         $Id$
-    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
 
-Executes miscellaneous examples for Higher-Order Logic. 
+Miscellaneous examples for Higher-Order Logic.
 *)
 
 (*some examples of recursive function definitions: the TFL package*)