# 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*)