diff -r fb201e383f1b -r da575186d492 Nominal/Ex/Sigma.thy --- a/Nominal/Ex/Sigma.thy Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -theory Sigma -imports Nominal2 -begin - -atom_decl name - -nominal_datatype obj = - Var name -| Obj smlst -| Inv obj string -| Upd obj string method -and smlst = - SMNil -| SMCons string method smlst -and method = - Sig n::name o::obj binds n in o - - -end -