equal
deleted
inserted
replaced
1 theory Let |
1 theory LetSimple2 |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 (* |
|
6 ML {* |
|
7 val lemma = |
|
8 Term_XML.Encode.term #> |
|
9 YXML.string_of_body #> |
|
10 translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #> |
|
11 quote #> prefix "lemma " #> |
|
12 Markup.markup Markup.sendback #> writeln |
|
13 *} |
|
14 |
|
15 ML {* lemma @{prop "x == x"} *} |
|
16 *) |
|
17 |
5 |
18 atom_decl name |
6 atom_decl name |
19 |
7 |
20 nominal_datatype trm = |
8 nominal_datatype trm = |
21 Var "name" |
9 Var "name" |