Nominal/Fv.thy
changeset 1774 c34347ec7ab3
parent 1744 00680cea0dde
child 1806 90095f23fc60
equal deleted inserted replaced
1773:c0eac04ae3b4 1774:c34347ec7ab3
     1 theory Fv
     1 theory Fv
     2 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"
     2 imports "../Nominal-General/Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"
     3 begin
     3 begin
     4 
     4 
     5 (* The bindings data structure:
     5 (* The bindings data structure:
     6 
     6 
     7   Bindings are a list of lists of lists of triples.
     7   Bindings are a list of lists of lists of triples.