equal
deleted
inserted
replaced
4 Introduces the lprod relation. |
4 Introduces the lprod relation. |
5 See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
5 See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
6 *) |
6 *) |
7 |
7 |
8 theory LProd |
8 theory LProd |
9 imports Multiset |
9 imports "~~/src/HOL/Library/Multiset" |
10 begin |
10 begin |
11 |
11 |
12 inductive_set |
12 inductive_set |
13 lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set" |
13 lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set" |
14 for R :: "('a * 'a) set" |
14 for R :: "('a * 'a) set" |