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/HOL/MicroJava/ROOT.ML
author wenzelm
Tue, 10 Jun 2008 19:15:18 +0200
changeset 27125 0733f575b51e
parent 24073 373727835757
child 27680 5a557a5afc48
permissions -rw-r--r--
tuned proofs -- case_tac *is* available here;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24073
373727835757 simultaneous use_thys;
wenzelm
parents: 13672
diff changeset 
     1
 
(* $Id$ *)
10631
591ea23d27a0 removed Digest (temporarily, not up to date)
kleing
parents: 10611
diff changeset 
     2
 







12911






704713ca07ea
new document



kleing


parents: 
12786

diff
changeset




     3


no_document use_thy "While_Combinator";













704713ca07ea
new document



kleing


parents: 
12786

diff
changeset




     4









24073






373727835757
simultaneous use_thys;



wenzelm


parents: 
13672

diff
changeset




     5


use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",













373727835757
simultaneous use_thys;



wenzelm


parents: 
13672

diff
changeset




     6


  "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",













373727835757
simultaneous use_thys;



wenzelm


parents: 
13672

diff
changeset




     7


  "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",













373727835757
simultaneous use_thys;



wenzelm


parents: 
13672

diff
changeset




     8


  "Comp/CorrCompTp"];















isabelle