# HG changeset patch # User wenzelm # Date 1298390774 -3600 # Node ID 6d4c3ee8219dde3d9b2d7f2d8a96d7d72d58e0fd # Parent c7be23634728c7a74bcd7085c62c2a782b0b678c modernized specifications; diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Hahn_Banach/Function_Order.thy --- a/src/HOL/Hahn_Banach/Function_Order.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Feb 22 17:06:14 2011 +0100 @@ -21,7 +21,7 @@ graph. *} -types 'a graph = "('a \ real) set" +type_synonym 'a graph = "('a \ real) set" definition graph :: "'a set \ ('a \ real) \ 'a graph" where diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Induct/Com.thy Tue Feb 22 17:06:14 2011 +0100 @@ -10,7 +10,7 @@ theory Com imports Main begin typedecl loc -types state = "loc => nat" +type_synonym state = "loc => nat" datatype exp = N nat diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Induct/Sexp.thy --- a/src/HOL/Induct/Sexp.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Induct/Sexp.thy Tue Feb 22 17:06:14 2011 +0100 @@ -8,8 +8,7 @@ theory Sexp imports Main begin -types - 'a item = "'a Datatype.item" +type_synonym 'a item = "'a Datatype.item" abbreviation "Leaf == Datatype.Leaf" abbreviation "Numb == Datatype.Numb" diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Isar_Examples/Expr_Compiler.thy --- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Feb 22 17:06:14 2011 +0100 @@ -22,8 +22,7 @@ This is both for abstract syntax and semantics, i.e.\ we use a ``shallow embedding'' here. *} -types - 'val binop = "'val => 'val => 'val" +type_synonym 'val binop = "'val => 'val => 'val" subsection {* Expressions *} diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Feb 22 17:06:14 2011 +0100 @@ -19,9 +19,8 @@ \cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and \cite{Nipkow:1998:Winskel}. *} -types - 'a bexp = "'a set" - 'a assn = "'a set" +type_synonym 'a bexp = "'a set" +type_synonym 'a assn = "'a set" datatype 'a com = Basic "'a => 'a" @@ -32,8 +31,7 @@ abbreviation Skip ("SKIP") where "SKIP == Basic id" -types - 'a sem = "'a => 'a => bool" +type_synonym 'a sem = "'a => 'a => bool" primrec iter :: "nat => 'a bexp => 'a sem => 'a sem" where diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Isar_Examples/Hoare_Ex.thy --- a/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Feb 22 16:47:18 2011 +0100 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Feb 22 17:06:14 2011 +0100 @@ -256,7 +256,7 @@ record tstate = time :: nat -types 'a time = "\time :: nat, \ :: 'a\" +type_synonym 'a time = "\time :: nat, \ :: 'a\" primrec timeit :: "'a time com \ 'a time com" where