equal
deleted
inserted
replaced
114 |
114 |
115 (*******************************) |
115 (*******************************) |
116 |
116 |
117 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); |
117 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); |
118 |
118 |
119 fun read_typ sign ((Ts, sorts), str) = |
|
120 let |
|
121 val T = Type.no_tvars (Sign.read_def_typ (sign, (AList.lookup op =) |
|
122 (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg |
|
123 in (Ts @ [T], add_typ_tfrees (T, sorts)) end; |
|
124 |
119 |
125 (** simplification procedure for sorting permutations **) |
120 (** simplification procedure for sorting permutations **) |
126 |
121 |
127 val dj_cp = thm "dj_cp"; |
122 val dj_cp = thm "dj_cp"; |
128 |
123 |
2014 |
2009 |
2015 in |
2010 in |
2016 thy13 |
2011 thy13 |
2017 end; |
2012 end; |
2018 |
2013 |
2019 val add_nominal_datatype = gen_add_nominal_datatype read_typ true; |
2014 val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true; |
2020 |
2015 |
2021 |
2016 |
2022 (* FIXME: The following stuff should be exported by DatatypePackage *) |
2017 (* FIXME: The following stuff should be exported by DatatypePackage *) |
2023 |
2018 |
2024 local structure P = OuterParse and K = OuterKeyword in |
2019 local structure P = OuterParse and K = OuterKeyword in |