Mercurial Mercurial > repos > isabelle / 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.
src/Doc/Tutorial/ToyList/ToyList_Test.thy
author traytel
Mon, 01 Sep 2014 14:14:47 +0200
changeset 58443 a23780c22245
parent 58372 bfd497f2f4c2
child 58856 4fced55fc5b7
permissions -rw-r--r--
goal generation for xtor_co_rec_transfer
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53376
1d4a46f1fced more robust ToyList_Test;
wenzelm
parents:
diff changeset 
     1
 
theory ToyList_Test
58372
bfd497f2f4c2 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents: 58112
diff changeset 
     2
 
imports BNF_Least_Fixpoint
53376
1d4a46f1fced more robust ToyList_Test;
wenzelm
parents:
diff changeset 
     3
 
begin
1d4a46f1fced more robust ToyList_Test;
wenzelm
parents:
diff changeset 
     4
 







57626






2288a6f17930
more official Thy_Info.script_thy;



wenzelm


parents: 
57083

diff
changeset




     5


ML {*













2288a6f17930
more official Thy_Info.script_thy;



wenzelm


parents: 
57083

diff
changeset




     6


  map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)













2288a6f17930
more official Thy_Info.script_thy;



wenzelm


parents: 
57083

diff
changeset




     7


    ["ToyList1.txt", "ToyList2.txt"]













2288a6f17930
more official Thy_Info.script_thy;



wenzelm


parents: 
57083

diff
changeset




     8


  |> implode













2288a6f17930
more official Thy_Info.script_thy;



wenzelm


parents: 
57083

diff
changeset




     9


  |> Thy_Info.script_thy Position.start








53376






1d4a46f1fced
more robust ToyList_Test;



wenzelm


parents: 

diff
changeset




    10


*}













1d4a46f1fced
more robust ToyList_Test;



wenzelm


parents: 

diff
changeset




    11














1d4a46f1fced
more robust ToyList_Test;



wenzelm


parents: 

diff
changeset




    12


end















isabelle