src/HOLCF/domain/interface.ML
author regensbu
Tue, 17 Oct 1995 17:59:47 +0100
changeset 1286 ae25649cbbb1
parent 1284 e5b95ee2616b
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     1
(* interface.ML
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     2
   ID:         $Id$
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     3
   Author:      David von Oheimb
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     4
   Created: 17-May-95
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     5
   Updated: 24-May-95
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     6
   Updated: 03-Jun-95 incremental change of ThySyn
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     7
   Updated: 11-Jul-95 use of ThyOps for cinfixes
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     8
   Updated: 21-Jul-95 gen_by-section
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     9
   Updated: 29-Aug-95 simultaneous domain equations
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    10
   Updated: 25-Aug-95 better syntax for simultaneous domain equations
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    11
   Copyright 1995 TU Muenchen
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    12
*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    13
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    14
local
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    15
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    16
structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData!!!!!!! *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    17
struct
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    18
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    19
local 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    20
  open ThyParse;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    21
  open Domain_Library;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    22
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    23
(* ----- generation of bindings for axioms and theorems in trailer of .thy.ML ----- *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    24
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    25
  fun gt_ax         name   = "get_axiom thy "^quote name;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    26
  fun gen_val dname name   = "val "^name^" = " ^gt_ax (dname^"_"^name)^";";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    27
  fun gen_vall      name l = "val "^name^" = " ^mk_list l^";";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    28
  val rews1 = "iso_rews @ when_rews @\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    29
 	      \con_rews @ sel_rews @ dis_rews @ dists_eq @ dists_le @\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    30
	      \copy_rews";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    31
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    32
  fun gen_domain eqname num ((dname,_), cons') = let
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    33
    val axioms1 = ["abs_iso", "rep_iso", "when_def"];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    34
		   (* con_defs , sel_defs, dis_defs *) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    35
    val axioms2 = ["copy_def"];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    36
    val theorems = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    37
	"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n    \
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    38
	\dists_eq, dists_le, inverts, injects, copy_rews";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    39
    in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    40
      "structure "^dname^" = struct\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    41
      cat_lines(map (gen_val dname) axioms1)^"\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    42
      gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    43
      gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    44
					     gt_ax(sel^"_def")) args)    cons'))^"\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    45
      gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    46
								          cons')^"\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    47
      cat_lines(map (gen_val dname) axioms2)^"\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    48
      "val ("^ theorems ^") =\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    49
      \Domain_Theorems.theorems thy "^eqname^";\n" ^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    50
      (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    51
    end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    52
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    53
  fun mk_domain (eqs'') = let
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    54
    val dtnvs  = map (type_name_vars o fst) eqs'';
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    55
    val dnames = map fst dtnvs;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    56
    val num = length dnames;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    57
    val comp_dname = implode (separate "_" dnames);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    58
    val conss' = map (fn (dname,cons'') =>
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    59
      let
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    60
	fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    61
							 "_"^(string_of_int m)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    62
				  |  Some s => s)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    63
	fun fill_sels n con = upd_third (mapn (sel n) 1) con;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    64
      in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    65
    val eqs' = dtnvs~~conss';
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    66
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    67
(* ----- generation of argument string for calling add_domain --------------------- *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    68
1284
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    69
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    70
     fun string_of_sort_emb [] = ""
1286
ae25649cbbb1 *** empty log message ***
regensbu
parents: 1284
diff changeset
    71
     |   string_of_sort_emb [x] = "\"" ^x^ "\"" 
ae25649cbbb1 *** empty log message ***
regensbu
parents: 1284
diff changeset
    72
	|   string_of_sort_emb (x::xs) = "\"" ^x^ "\"" ^ ", "^(string_of_sort_emb xs);
1284
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    73
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    74
	fun string_of_sort l = "["^ (string_of_sort_emb l)^"]";
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    75
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    76
    fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v))
1284
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
    77
    and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    78
    |   mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    79
    |   mk_typ _                  = Imposs "interface:mk_typ";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    80
    fun mk_conslist cons' = mk_list (map 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    81
	  (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    82
     (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s,
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    83
				    mk_typ tp)) ts))) cons');
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    84
    in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    85
      ("val (thy, "^comp_dname^"_equations) = thy |> Extender.add_domain \n"
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    86
      ^ mk_pair(quote comp_dname,
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    87
		mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    88
      ^ ";\nval thy = thy",
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    89
      let
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    90
	fun plural s = if num > 1 then s^"s" else "["^s^"]";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    91
	val comp_axioms   = [(* copy, *) "take_def", "finite_def", "reach" 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    92
			     (*, "bisim_def" *)];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    93
	val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    94
				["take_lemma","finite"]))^", finite_ind, ind, coind";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    95
	fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), "
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    96
							   ^comp_dname^"_equations)";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    97
	fun collect sep name = if num = 1 then name else
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    98
			   implode (separate sep (map (fn s => s^"."^name) dnames));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    99
      in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   100
	implode (separate "end; (* struct *)\n\n" 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   101
		 (mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   102
	"end; (* struct *)\n\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   103
	\structure "^comp_dname^" = struct\n" else "") ^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   104
	 (if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   105
	 implode ((map (fn s => gen_vall (plural s)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   106
		  (map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   107
	 gen_val comp_dname "bisim_def" ^"\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   108
        \val ("^ comp_theorems ^") =\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   109
	\Domain_Theorems.comp_theorems thy \
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   110
	\(" ^ quote comp_dname   ^ ","^ comp_dname ^"_equations,\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   111
	\ ["^collect "," "cases"    ^"],\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   112
	\ "^ collect "@" "con_rews " ^",\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   113
	\ "^ collect "@" "copy_rews" ^");\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   114
	\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   115
	\end; (* struct *)"
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   116
      end
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   117
      ) end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   118
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   119
  fun mk_gen_by (finite,eqs) = let
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   120
      val typs    = map fst eqs;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   121
      val cnstrss = map snd eqs;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   122
      val tname = implode (separate "_" typs) in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   123
      ("|> Extender.add_gen_by "
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   124
      ^ mk_pair(mk_pair(quote tname,makestring (finite:bool)),
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   125
		mk_pair(mk_list(map quote typs), 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   126
			mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))),
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   127
      "val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   128
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   129
(* ----- parser for domain declaration equation ----------------------------------- *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   130
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   131
(**
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   132
  val sort = name >> (fn s => [strip_quotes s])
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   133
	  || "{" $$-- !! (list (name >> strip_quotes) --$$ "}");
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   134
  val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   135
**)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   136
  val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   137
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   138
  val type_args = "(" $$-- !! (list1 tvar --$$ ")")
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   139
	       || tvar  >> (fn x => [x])
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   140
	       || empty >> K [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   141
  val con_typ     = type_args -- ident >> (fn (x,y) => Type(y,x));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   142
  val typ         = con_typ 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   143
		 || tvar;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   144
  val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   145
			  -- (optional ((ident >> Some) --$$ "::") None)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   146
			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   147
		 || ident >> (fn x => (false,None,Type(x,[])))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   148
		 || tvar  >> (fn x => (false,None,x));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   149
  val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   150
		    -- ThyOps.opt_cmixfix
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   151
		    >> (fn ((con,args),syn) => (con,syn,args));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   152
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   153
  val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   154
			       (enum1 "|" domain_cons))) 	    >> mk_domain;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   155
  val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   156
		    (enum1 "," (ident   --$$ "by" -- !!
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   157
			       (enum1 "|" (name >> strip_quotes)))) >> mk_gen_by;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   158
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   159
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   160
val user_keywords = "lazy"::"by"::"finite"::
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   161
		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   162
		    ThySynData.user_keywords;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   163
val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   164
		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   165
		    ThySynData.user_sections;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   166
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   167
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   168
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   169
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   170
structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   171
1284
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
   172
end; (* local *)
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
   173