--- a/src/HOL/Subst/UTLemmas.thy Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/Subst/UTLemmas.thy Fri Dec 01 13:03:34 1995 +0100
@@ -9,8 +9,8 @@
consts
- vars_of :: "'a uterm=>'a set"
- "<:" :: "['a uterm,'a uterm]=>bool" (infixl 54)
+ vars_of :: 'a uterm=>'a set
+ "<:" :: ['a uterm,'a uterm]=>bool (infixl 54)
rules (*Definitions*)
--- a/src/HOL/Subst/UTerm.thy Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/Subst/UTerm.thy Fri Dec 01 13:03:34 1995 +0100
@@ -23,10 +23,10 @@
Var :: 'a => 'a uterm
Const :: 'a => 'a uterm
Comb :: ['a uterm, 'a uterm] => 'a uterm
- UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b,
- ['a item , 'a item, 'b, 'b]=>'b] => 'b"
- uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b,
- ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
+ UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b,
+ ['a item , 'a item, 'b, 'b]=>'b] => 'b
+ uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b,
+ ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
defs
(*defining the concrete constructors*)
--- a/src/HOL/ex/Simult.thy Fri Dec 01 12:27:09 1995 +0100
+++ b/src/HOL/ex/Simult.thy Fri Dec 01 13:03:34 1995 +0100
@@ -31,12 +31,12 @@
Tcons :: ['a, 'a forest] => 'a tree
Fcons :: ['a tree, 'a forest] => 'a forest
Fnil :: 'a forest
- TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b,
- 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
- tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b,
- 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
- forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b,
- 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+ TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b,
+ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
+ tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
+ forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
defs
(*the concrete constants*)