equal
deleted
inserted
replaced
917 @{ML_response_fake [display,gray] |
917 @{ML_response_fake [display,gray] |
918 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
918 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
919 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
919 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
920 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
920 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
921 |
921 |
922 (FIXME: readmore about types) |
922 (FIXME: a readmore about types) |
923 *} |
923 *} |
924 |
924 |
925 |
925 |
926 section {* Type-Checking *} |
926 section {* Type-Checking *} |
927 |
927 |
1112 @{ML_file "Pure/thm.ML"}. |
1112 @{ML_file "Pure/thm.ML"}. |
1113 \end{readmore} |
1113 \end{readmore} |
1114 |
1114 |
1115 (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on) |
1115 (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on) |
1116 |
1116 |
1117 (FIXME how to add case-names to goal states - maybe in the |
1117 (FIXME: how to add case-names to goal states - maybe in the |
1118 next section) |
1118 next section) |
1119 *} |
1119 *} |
1120 |
1120 |
1121 section {* Theorem Attributes *} |
1121 section {* Theorem Attributes *} |
1122 |
1122 |