Mercurial Mercurial > hg > isabelle-cookbook / comparison
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/Parsing.thy
changeset 366 06f044466f24
parent 361 8ba963a3e039
child 369 74ba778b09c9
equal deleted inserted replaced
365:718beb785213 366:06f044466f24 
  1132 ML {*
 
  1132 ML {*
 
  1133 structure TacticData = ProofDataFun
 
  1133 structure TacticData = ProofDataFun
 
  1134 (
 
  1134 (
 
  1135   type T = thm list -> tactic;
 
  1135   type T = thm list -> tactic;
 
  1136   fun init _ = undefined;
 
  1136   fun init _ = undefined;
 
  1137 );
 
  1137 )
 
  1138 
  1138 
  1139 val set_tactic = TacticData.put;
 
  1139 val set_tactic = TacticData.put;
 
  1140 *}
 
  1140 *}
 
  1141 
  1141 
  1142 ML {*
 
  1142 ML {*
isabelle-cookbook