--- 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
--- 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.
*)
--- 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
--- 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
--- 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 *}
--- 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*)