doc-src/IsarRef/basics.tex
author wenzelm
Fri, 15 Jul 2005 15:44:11 +0200
changeset 16860 43abdba4da5c
parent 7981 5120a2a15d06
permissions -rw-r--r--
* Pure/library.ML: several combinators for linear functional transformations; * Pure/library.ML: canonical list combinators fold, fold_rev, and fold_yield; * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
7981
wenzelm
parents: 7895
diff changeset
     2
%FIXME
wenzelm
parents: 7895
diff changeset
     3
%\chapter{Basic Concepts}\label{ch:basics}
wenzelm
parents: 7895
diff changeset
     4
%\section{The Isar proof language}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     5
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     6
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     7
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     8
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     9
%%% End: