# HG changeset patch # User Walther Neuper # Date 1279788318 -7200 # Node ID 331e38464ada88bb8552be6f02f996e3de1893b1 # Parent 2fcd710fe1d0896a7e14b235664eba8ccf1eea01# Parent b553ca89e7eb9e4ac89119522c17419674ee589f merged diff -r 2fcd710fe1d0 -r 331e38464ada README_REPOSITORY --- a/README_REPOSITORY Thu Jul 22 10:40:19 2010 +0200 +++ b/README_REPOSITORY Thu Jul 22 10:45:18 2010 +0200 @@ -1,9 +1,13 @@ 100721 download Isabelle repository + install runnable system ===========================================================WN -# clone the repository - /usr/local$ sudo hg clone http://isabelle.in.tum.de/repos/isabelle isabisac - /usr/local/isabisac$ sudo chown -r neuper * #become owner +# clone the munich repository + #/usr/local$ sudo hg clone http://isabelle.in.tum.de/repos/isabelle isabisac + +# clone the IST repository + /usr/local$ sudo hg clone -U https://intra.ist.tugraz.at/hg/isa/ isabisac #changesets + /usr/local/isabisac$ sudo hg update -C 875b6efa7ced #from tip ??why nothttps://.. + /usr/local/isabisac$ sudo chown -R neuper * #become owner hg update -C Isabelle2009-2 #go to release hg branch isac-from-Isabelle2009-2 #make branch hg ci #commit diff -r 2fcd710fe1d0 -r 331e38464ada src/Pure/isac/#Isac_Mathengine.thy# --- a/src/Pure/isac/#Isac_Mathengine.thy# Thu Jul 22 10:40:19 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -(* Title: ~~~/isac/Isac_Mathengine.thy - Author: Walther Neuper, TU Graz - -$ cd /usr/local/Isabelle2009-1/src/Pure/isac -$ /usr/local/Isabelle2009-1/bin/isabelle emacs Isac_Mathengine.thy & - -OR tty (unusable: after errors wrong toplevel): -$ cd "/home/neuper/proto2/isac/src/sml" -$ isabelle-process HOL HOL-Isac -ML> use_thy "Isac_Mathengine"; -*) - -header {* Loading the isac mathengine *} - -theory Isac_Mathengine -imports Complex_Main -(*imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)*) -begin - -ML {* 1.2;3.4;5; *} - -use "library.sml" -use "calcelems.sml" -ML {* check_guhs_unique := true *} - -use "Scripts/term_G.sml" -use "Scripts/calculate.sml" - -use "Scripts/rewrite.sml" -(* -use_thy"Scripts/Script" -use "Scripts/ListG.ML" -use "Scripts/Tools.ML" -use "Scripts/Script.ML" - -use "Scripts/scrtools.sml" - -use "ME/mstools.sml" -use "ME/ctree.sml" -use "ME/ptyps.sml" -use "ME/generate.sml" -use "ME/calchead.sml" -use "ME/appl.sml" -use "ME/rewtools.sml" -use "ME/script.sml" -use "ME/solve.sml" -use "ME/inform.sml" -use "ME/mathengine.sml" - -use "xmlsrc/mathml.sml" -use "xmlsrc/datatypes.sml" -use "xmlsrc/pbl-met-hierarchy.sml" -use "xmlsrc/thy-hierarchy.sml" -use "xmlsrc/interface-xml.sml" - -use "FE-interface/messages.sml" -use "FE-interface/states.sml" -use "FE-interface/interface.sml" - -use "print_exn_G.sml" - -text "**** build math-engine complete *************************" -*)(* -setup {* - Code_Preproc.setup - #> Code_ML.setup - #> Code_Haskell.setup - #> Nbe.setup -*} -*) - - -(*cleaner output from...*) -ML_command {* -"----- "; -writeln "werwerw"; -*} - -ML {* @{prop "False"} *} -(*ML {* @{type "int"} *} only new version*) -ML {* @{thm conjI} *} -ML {* @{thms conjI TrueI} *} -ML {* @{theory} *} - -ML{* @{const_name plus} *} (*creates long names (extern names)*) -term plus - -term foo -(*ML{* @{const_name foo} *} only new version*) - -text {* -werwer - *} - -ML {* - fun inc_by_five x = - x |> (fn x => x + 1) -*} - -(*canonical argument order introduced after 1997*) - -text{* -this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold)) -@{ML fold} - -@{ML fold_rev} - -for accumulating side results in |> -@{ML fold_map} -*} - -ML {* - val items = 1 upto 10; - val l1 = fold cons items []; (*alternating useful frequently*) -*} - -ML{* - fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs; -*} -ML{* - merge_list (op =) ([3,2,1], [7,5,3,1]); - merge_list (op =) ([3,2,1], [7,5,3,1]); -*} - -(*session 2-------Christian+Makarius---------------*) -ML{* -let - val ctxt = @{context} -in 1 end -*} - -(* build and handle tables THIS IS THE ACCESS-STRUCTURE... -ML{* - structure Data = Theory_Data - ( - type T = term Symtab.table - val empty = Symtab.empty - val extend = O - fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2) - ) -*} -*) -(*session 3-------Blanchette-------------------- -working on nitpic, ML level tool - -SEE THESE LECTURE NOTES !!!*) - -(* -ML{* -Const ("x", dummyT) |> Syntax.check_term @{context} - ^^^^^^^^^^^^^^^^^ -*} -*) - -text{* -SEE funs for -# deleting identifiers -# handle Bounds when made visible -# kill trivial quantifiers, e.g. \foral x. (NO x) -# handling name clashes in Abs -# which constants, free vars ... occur in a term !!!!!!!!!!! -# Var (("x", 2), dummyT) ... 25 old from Larry "maxidx" -# get fresh Const, Var -# use the "Name" structure - -*} - -ML{* val context = Name.make_context ["d"] *} - -(* -ML{* Name.invents context "foo" 10 *} -(*ML{* Name variants ... *}*) -*) - -end - diff -r 2fcd710fe1d0 -r 331e38464ada src/Pure/isac/Isac_Mathengine.thy --- a/src/Pure/isac/Isac_Mathengine.thy Thu Jul 22 10:40:19 2010 +0200 +++ b/src/Pure/isac/Isac_Mathengine.thy Thu Jul 22 10:45:18 2010 +0200 @@ -1,8 +1,9 @@ (* Title: ~~~/isac/Isac_Mathengine.thy Author: Walther Neuper, TU Graz -$ cd /usr/local/isabisac/src/Pure/isac +$ cd /usr/local/Isabelle2009-1/src/Pure/isac $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy & +$ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy & OR tty (unusable: after errors wrong toplevel): $ cd "/home/neuper/proto2/isac/src/sml" @@ -13,7 +14,8 @@ header {* Loading the isac mathengine *} theory Isac_Mathengine -imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*) +imports Complex_Main +(*imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)*) begin ML {* 1.2;3.4;5; *} @@ -26,8 +28,8 @@ use "Scripts/calculate.sml" use "Scripts/rewrite.sml" +(* use_thy"Scripts/Script" -(* use "Scripts/ListG.ML" use "Scripts/Tools.ML" use "Scripts/Script.ML"