1.1 --- a/README_REPOSITORY Thu Jul 22 10:40:19 2010 +0200
1.2 +++ b/README_REPOSITORY Thu Jul 22 10:45:18 2010 +0200
1.3 @@ -1,9 +1,13 @@
1.4 100721 download Isabelle repository + install runnable system
1.5 ===========================================================WN
1.6
1.7 -# clone the repository
1.8 - /usr/local$ sudo hg clone http://isabelle.in.tum.de/repos/isabelle isabisac
1.9 - /usr/local/isabisac$ sudo chown -r neuper * #become owner
1.10 +# clone the munich repository
1.11 + #/usr/local$ sudo hg clone http://isabelle.in.tum.de/repos/isabelle isabisac
1.12 +
1.13 +# clone the IST repository
1.14 + /usr/local$ sudo hg clone -U https://intra.ist.tugraz.at/hg/isa/ isabisac #changesets
1.15 + /usr/local/isabisac$ sudo hg update -C 875b6efa7ced #from tip ??why nothttps://..
1.16 + /usr/local/isabisac$ sudo chown -R neuper * #become owner
1.17 hg update -C Isabelle2009-2 #go to release
1.18 hg branch isac-from-Isabelle2009-2 #make branch
1.19 hg ci #commit
2.1 --- a/src/Pure/isac/#Isac_Mathengine.thy# Thu Jul 22 10:40:19 2010 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,176 +0,0 @@
2.4 -(* Title: ~~~/isac/Isac_Mathengine.thy
2.5 - Author: Walther Neuper, TU Graz
2.6 -
2.7 -$ cd /usr/local/Isabelle2009-1/src/Pure/isac
2.8 -$ /usr/local/Isabelle2009-1/bin/isabelle emacs Isac_Mathengine.thy &
2.9 -
2.10 -OR tty (unusable: after errors wrong toplevel):
2.11 -$ cd "/home/neuper/proto2/isac/src/sml"
2.12 -$ isabelle-process HOL HOL-Isac
2.13 -ML> use_thy "Isac_Mathengine";
2.14 -*)
2.15 -
2.16 -header {* Loading the isac mathengine *}
2.17 -
2.18 -theory Isac_Mathengine
2.19 -imports Complex_Main
2.20 -(*imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)*)
2.21 -begin
2.22 -
2.23 -ML {* 1.2;3.4;5; *}
2.24 -
2.25 -use "library.sml"
2.26 -use "calcelems.sml"
2.27 -ML {* check_guhs_unique := true *}
2.28 -
2.29 -use "Scripts/term_G.sml"
2.30 -use "Scripts/calculate.sml"
2.31 -
2.32 -use "Scripts/rewrite.sml"
2.33 -(*
2.34 -use_thy"Scripts/Script"
2.35 -use "Scripts/ListG.ML"
2.36 -use "Scripts/Tools.ML"
2.37 -use "Scripts/Script.ML"
2.38 -
2.39 -use "Scripts/scrtools.sml"
2.40 -
2.41 -use "ME/mstools.sml"
2.42 -use "ME/ctree.sml"
2.43 -use "ME/ptyps.sml"
2.44 -use "ME/generate.sml"
2.45 -use "ME/calchead.sml"
2.46 -use "ME/appl.sml"
2.47 -use "ME/rewtools.sml"
2.48 -use "ME/script.sml"
2.49 -use "ME/solve.sml"
2.50 -use "ME/inform.sml"
2.51 -use "ME/mathengine.sml"
2.52 -
2.53 -use "xmlsrc/mathml.sml"
2.54 -use "xmlsrc/datatypes.sml"
2.55 -use "xmlsrc/pbl-met-hierarchy.sml"
2.56 -use "xmlsrc/thy-hierarchy.sml"
2.57 -use "xmlsrc/interface-xml.sml"
2.58 -
2.59 -use "FE-interface/messages.sml"
2.60 -use "FE-interface/states.sml"
2.61 -use "FE-interface/interface.sml"
2.62 -
2.63 -use "print_exn_G.sml"
2.64 -
2.65 -text "**** build math-engine complete *************************"
2.66 -*)(*
2.67 -setup {*
2.68 - Code_Preproc.setup
2.69 - #> Code_ML.setup
2.70 - #> Code_Haskell.setup
2.71 - #> Nbe.setup
2.72 -*}
2.73 -*)
2.74 -
2.75 -
2.76 -(*cleaner output from...*)
2.77 -ML_command {*
2.78 -"----- ";
2.79 -writeln "werwerw";
2.80 -*}
2.81 -
2.82 -ML {* @{prop "False"} *}
2.83 -(*ML {* @{type "int"} *} only new version*)
2.84 -ML {* @{thm conjI} *}
2.85 -ML {* @{thms conjI TrueI} *}
2.86 -ML {* @{theory} *}
2.87 -
2.88 -ML{* @{const_name plus} *} (*creates long names (extern names)*)
2.89 -term plus
2.90 -
2.91 -term foo
2.92 -(*ML{* @{const_name foo} *} only new version*)
2.93 -
2.94 -text {*
2.95 -werwer
2.96 - *}
2.97 -
2.98 -ML {*
2.99 - fun inc_by_five x =
2.100 - x |> (fn x => x + 1)
2.101 -*}
2.102 -
2.103 -(*canonical argument order introduced after 1997*)
2.104 -
2.105 -text{*
2.106 -this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
2.107 -@{ML fold}
2.108 -
2.109 -@{ML fold_rev}
2.110 -
2.111 -for accumulating side results in |>
2.112 -@{ML fold_map}
2.113 -*}
2.114 -
2.115 -ML {*
2.116 - val items = 1 upto 10;
2.117 - val l1 = fold cons items []; (*alternating useful frequently*)
2.118 -*}
2.119 -
2.120 -ML{*
2.121 - fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
2.122 -*}
2.123 -ML{*
2.124 - merge_list (op =) ([3,2,1], [7,5,3,1]);
2.125 - merge_list (op =) ([3,2,1], [7,5,3,1]);
2.126 -*}
2.127 -
2.128 -(*session 2-------Christian+Makarius---------------*)
2.129 -ML{*
2.130 -let
2.131 - val ctxt = @{context}
2.132 -in 1 end
2.133 -*}
2.134 -
2.135 -(* build and handle tables THIS IS THE ACCESS-STRUCTURE...
2.136 -ML{*
2.137 - structure Data = Theory_Data
2.138 - (
2.139 - type T = term Symtab.table
2.140 - val empty = Symtab.empty
2.141 - val extend = O
2.142 - fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
2.143 - )
2.144 -*}
2.145 -*)
2.146 -(*session 3-------Blanchette--------------------
2.147 -working on nitpic, ML level tool
2.148 -
2.149 -SEE THESE LECTURE NOTES !!!*)
2.150 -
2.151 -(*
2.152 -ML{*
2.153 -Const ("x", dummyT) |> Syntax.check_term @{context}
2.154 - ^^^^^^^^^^^^^^^^^
2.155 -*}
2.156 -*)
2.157 -
2.158 -text{*
2.159 -SEE funs for
2.160 -# deleting identifiers
2.161 -# handle Bounds when made visible
2.162 -# kill trivial quantifiers, e.g. \foral x. (NO x)
2.163 -# handling name clashes in Abs
2.164 -# which constants, free vars ... occur in a term !!!!!!!!!!!
2.165 -# Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
2.166 -# get fresh Const, Var
2.167 -# use the "Name" structure
2.168 -
2.169 -*}
2.170 -
2.171 -ML{* val context = Name.make_context ["d"] *}
2.172 -
2.173 -(*
2.174 -ML{* Name.invents context "foo" 10 *}
2.175 -(*ML{* Name variants ... *}*)
2.176 -*)
2.177 -
2.178 -end
2.179 -
3.1 --- a/src/Pure/isac/Isac_Mathengine.thy Thu Jul 22 10:40:19 2010 +0200
3.2 +++ b/src/Pure/isac/Isac_Mathengine.thy Thu Jul 22 10:45:18 2010 +0200
3.3 @@ -1,8 +1,9 @@
3.4 (* Title: ~~~/isac/Isac_Mathengine.thy
3.5 Author: Walther Neuper, TU Graz
3.6
3.7 -$ cd /usr/local/isabisac/src/Pure/isac
3.8 +$ cd /usr/local/Isabelle2009-1/src/Pure/isac
3.9 $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
3.10 +$ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
3.11
3.12 OR tty (unusable: after errors wrong toplevel):
3.13 $ cd "/home/neuper/proto2/isac/src/sml"
3.14 @@ -13,7 +14,8 @@
3.15 header {* Loading the isac mathengine *}
3.16
3.17 theory Isac_Mathengine
3.18 -imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
3.19 +imports Complex_Main
3.20 +(*imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)*)
3.21 begin
3.22
3.23 ML {* 1.2;3.4;5; *}
3.24 @@ -26,8 +28,8 @@
3.25 use "Scripts/calculate.sml"
3.26
3.27 use "Scripts/rewrite.sml"
3.28 +(*
3.29 use_thy"Scripts/Script"
3.30 -(*
3.31 use "Scripts/ListG.ML"
3.32 use "Scripts/Tools.ML"
3.33 use "Scripts/Script.ML"