equal
deleted
inserted
replaced
1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList |
2 imports QuotScript QuotList Prove |
3 begin |
3 begin |
|
4 |
|
5 (* |
|
6 prove {* @{prop "True"} *} |
|
7 apply(rule TrueI) |
|
8 done |
|
9 *) |
4 |
10 |
5 locale QUOT_TYPE = |
11 locale QUOT_TYPE = |
6 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
12 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
7 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
13 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
8 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
14 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |