Mercurial Mercurial > hg > isabelle-cookbook / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/document/root.rao
author Christian Urban <urbanc@in.tum.de>
Sat, 23 May 2009 02:19:54 +0200
changeset 252 f380b13b25a7
parent 218 7ff7325e3b4e
permissions -rw-r--r--
added an example
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset 
     1
 
% This file was generated by 'rail' from 'ProgTutorial/generated/root.rai'
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset 
     2
 
\rail@t {simpleinductive}
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset 
     3
 
\rail@t {where}
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset 
     4
 
\rail@t {for}
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset 
     5
 
\rail@i {1}{ simpleinductive target?\\ fixes (where (thmdecl? prop + '|'))? ; }
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
     6
 
\rail@o {1}{
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
     7
 
\rail@begin{7}{}
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset 
     8
 
\rail@token{simpleinductive}[]
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
     9
 
\rail@bar
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    10
 
\rail@nextbar{1}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    11
 
\rail@nont{target}[]
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    12
 
\rail@endbar
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset 
    13
 
\rail@cr{3}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    14
 
\rail@nont{fixes}[]
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    15
 
\rail@bar
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    16
 
\rail@nextbar{4}
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset 
    17
 
\rail@token{where}[]
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    18
 
\rail@plus
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    19
 
\rail@bar
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    20
 
\rail@nextbar{5}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    21
 
\rail@nont{thmdecl}[]
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    22
 
\rail@endbar
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    23
 
\rail@nont{prop}[]
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    24
 
\rail@nextplus{6}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    25
 
\rail@cterm{|}[]
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    26
 
\rail@endplus
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    27
 
\rail@endbar
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    28
 
\rail@end
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset 
    29
 
}
isabelle-cookbook