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/Mirabelle/ex/Ex.thy
author haftmann
Wed, 21 Mar 2018 19:39:23 +0100
changeset 67907 02a14c1cb917
parent 67443 3abf6a722518
child 69043 57a76e4728ed
permissions -rw-r--r--
prefer convention to place operation name before type name
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48589
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
diff changeset 
     1
 
theory Ex imports Pure
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
diff changeset 
     2
 
begin
fb446a780d50 separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
diff changeset 
     3
 







63167






0909deb8059b
isabelle update_cartouches -c -t;



wenzelm


parents: 
62589

diff
changeset




     4


ML \<open>








48589






fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




     5


  val rc = Isabelle_System.bash








63971






da89140186e2
HOL-Analysis: move Product_Vector and Inner_Product from Library



hoelzl


parents: 
63167

diff
changeset




     6


    "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy";








48589






fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




     7


  if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)













fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




     8


  else ();








67443






3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;



wenzelm


parents: 
63971

diff
changeset




     9


\<close> \<comment> \<open>some arbitrary small test case\<close>








48589






fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




    10














fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




    11


end













fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;



wenzelm


parents: 

diff
changeset




    12
















isabelle