equal
deleted
inserted
replaced
169 |
169 |
170 |
170 |
171 section {* Combinators\label{sec:combinators} *} |
171 section {* Combinators\label{sec:combinators} *} |
172 |
172 |
173 text {* |
173 text {* |
174 (FIXME: maybe move before antiquotation section) |
|
175 |
|
176 For beginners, perhaps the most puzzling parts in the existing code of Isabelle are |
174 For beginners, perhaps the most puzzling parts in the existing code of Isabelle are |
177 the combinators. At first they seem to greatly obstruct the |
175 the combinators. At first they seem to greatly obstruct the |
178 comprehension of the code, but after getting familiar with them, they |
176 comprehension of the code, but after getting familiar with them, they |
179 actually ease the understanding and also the programming. |
177 actually ease the understanding and also the programming. |
180 |
|
181 \begin{readmore} |
|
182 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
|
183 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
|
184 contains further information about combinators. |
|
185 \end{readmore} |
|
186 |
178 |
187 The simplest combinator is @{ML I}, which is just the identity function defined as |
179 The simplest combinator is @{ML I}, which is just the identity function defined as |
188 *} |
180 *} |
189 |
181 |
190 ML{*fun I x = x*} |
182 ML{*fun I x = x*} |
339 #-> (fn x => fn y => x + y)*} |
331 #-> (fn x => fn y => x + y)*} |
340 |
332 |
341 text {* |
333 text {* |
342 |
334 |
343 (FIXME: find a good exercise for combinators) |
335 (FIXME: find a good exercise for combinators) |
|
336 |
|
337 \begin{readmore} |
|
338 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
|
339 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
|
340 contains further information about combinators. |
|
341 \end{readmore} |
344 |
342 |
345 *} |
343 *} |
346 |
344 |
347 |
345 |
348 section {* Antiquotations *} |
346 section {* Antiquotations *} |
872 For the functions @{text "assume"}, @{text "forall_elim"} etc |
870 For the functions @{text "assume"}, @{text "forall_elim"} etc |
873 see \isccite{sec:thms}. The basic functions for theorems are defined in |
871 see \isccite{sec:thms}. The basic functions for theorems are defined in |
874 @{ML_file "Pure/thm.ML"}. |
872 @{ML_file "Pure/thm.ML"}. |
875 \end{readmore} |
873 \end{readmore} |
876 |
874 |
877 (FIXME: how to add case-names to goal states) |
875 (FIXME: how to add case-names to goal states - maybe in the next section) |
878 *} |
876 *} |
879 |
877 |
880 |
878 |
881 section {* Theorem Attributes *} |
879 section {* Theorem Attributes *} |
|
880 |
|
881 text {* |
|
882 |
|
883 |
|
884 If you want to print out all currently known attributes a theorem |
|
885 can have, you can use the function: |
|
886 |
|
887 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
|
888 "COMP: direct composition with rules (no lifting) |
|
889 HOL.dest: declaration of Classical destruction rule |
|
890 HOL.elim: declaration of Classical elimination rule |
|
891 \<dots>"} |
|
892 |
|
893 *} |
|
894 |
882 |
895 |
883 section {* Theories and Local Theories *} |
896 section {* Theories and Local Theories *} |
884 |
897 |
885 text {* |
898 text {* |
886 (FIXME: expand) |
899 (FIXME: expand) |