branch | Nominal2-Isabelle2013 |
changeset 3208 | da575186d492 |
parent 3206 | fb201e383f1b |
child 3209 | 2fb0bc0dcbf1 |
--- 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 -