Quot/Examples/FSet.thy
changeset 600 5d932e7a856c
parent 597 8a1c8dc72b5c
child 609 6ce4f274b0fa
child 610 2bee5ca44ef5
equal deleted inserted replaced
599:1e07e38ed6c5 600:5d932e7a856c
     1 theory FSet
     1 theory FSet
     2 imports "../QuotMain"
     2 imports "../QuotMain" List
     3 begin
     3 begin
     4 
     4 
     5 inductive
     5 inductive
     6   list_eq (infix "\<approx>" 50)
     6   list_eq (infix "\<approx>" 50)
     7 where
     7 where