--- a/Univ.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Univ.thy Thu Aug 25 11:01:45 1994 +0200
@@ -15,6 +15,7 @@
types
'a node
+ 'a item = "'a node set"
arities
node :: (term)term
@@ -31,25 +32,25 @@
Push_Node :: "[nat, 'a node] => 'a node"
ndepth :: "'a node => nat"
- Atom :: "('a+nat) => 'a node set"
- Leaf :: "'a => 'a node set"
- Numb :: "nat => 'a node set"
- "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
- In0,In1 :: "'a node set => 'a node set"
+ Atom :: "('a+nat) => 'a item"
+ Leaf :: "'a => 'a item"
+ Numb :: "nat => 'a item"
+ "$" :: "['a item, 'a item]=> 'a item" (infixr 60)
+ In0,In1 :: "'a item => 'a item"
- ntrunc :: "[nat, 'a node set] => 'a node set"
+ ntrunc :: "[nat, 'a item] => 'a item"
- "<*>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
- "<+>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
+ "<*>" :: "['a item set, 'a item set]=> 'a item set" (infixr 80)
+ "<+>" :: "['a item set, 'a item set]=> 'a item set" (infixr 70)
- Split :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
- Case :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
+ Split :: "[['a item, 'a item]=>'b, 'a item] => 'b"
+ Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
diag :: "'a set => ('a * 'a)set"
- "<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\ => ('a node set * 'a node set)set" (infixr 80)
- "<++>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\ => ('a node set * 'a node set)set" (infixr 70)
+ "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\ => ('a item * 'a item)set" (infixr 80)
+ "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\ => ('a item * 'a item)set" (infixr 70)
rules