diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_relation.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_relation.thy | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_relation.thy b/snapshots/isabelle/lib/lem/Lem_relation.thy index 23e7d707..778507a7 100644 --- a/snapshots/isabelle/lib/lem/Lem_relation.thy +++ b/snapshots/isabelle/lib/lem/Lem_relation.thy @@ -1,14 +1,14 @@ -chapter \<open>Generated by Lem from relation.lem.\<close> +chapter \<open>Generated by Lem from \<open>relation.lem\<close>.\<close> theory "Lem_relation" -imports - Main - "Lem_bool" - "Lem_basic_classes" - "Lem_tuple" - "Lem_set" - "Lem_num" +imports + Main + "Lem_bool" + "Lem_basic_classes" + "Lem_tuple" + "Lem_set" + "Lem_num" begin @@ -85,7 +85,7 @@ definition relFromPred :: " 'a set \<Rightarrow> 'b set \<Rightarrow>('a \<Righ (*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*) definition relIdOn :: " 'a set \<Rightarrow>('a*'a)set " where - " relIdOn s = ( relFromPred s s (op=))" + " relIdOn s = ( relFromPred s s (=))" (*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*) |