wneuper/isa: src/Tools/isac/Specify/Specify.thy@c5c128afdb00

     1 (* Title:  collect all defitions for the Lucas-Interpreter

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

     4  *)

     6 theory Specify

     7 imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript

     8 begin

     9 (* removed all warnings here, only "handle _" remains *)

    10   ML_file model.sml

    11   ML_file mstools.sml

    12   ML_file "specification-elems.sml"

    13   ML_file istate.sml

    14   ML_file tactic.sml

    15   ML_file "ctree-basic.sml" (*shift to base in common with Interpret*)

    16   ML_file "ctree-access.sml"(*shift to base in common with Interpret*)

    17   ML_file "ctree-navi.sml"  (*shift to base in common with Interpret*)

    18   ML_file ctree.sml         (*shift to base in common with Interpret*)

    19   ML_file ptyps.sml

    20   ML_file generate.sml

    21   ML_file calchead.sml

    22   ML_file appl.sml

    24 ML \<open>

    25 \<close> ML \<open>

    26 \<close> ML \<open>

    27 \<close>

    28 end

author	Walther Neuper <wneuper@ist.tugraz.at>
	Tue, 27 Aug 2019 15:31:45 +0200
changeset 59595	c5c128afdb00
parent 59594	8e357be69082
child 59674	3da177a07c3e
permissions	-rw-r--r--