wneuper/isa: src/Tools/isac/Interpret/Interpret.thy@c7b1a99bcfd2

     1 (* Title:  Interpret/Interpret.thy

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

     5 Collect all defitions for the Lucas-Interpreter

     6 *)

     8 theory Interpret

     9 imports Specify.Specify

    10 begin

    11   ML_file istate.sml

    12   ML_file "sub-problem.sml"

    13   ML_file "thy-read.sml"

    14   ML_file "solve-step.sml"

    15   ML_file "error-pattern.sml"

    16   ML_file derive.sml

    17   ML_file "li-tool.sml"

    18   ML_file "lucas-interpreter.sml"

    19   ML_file "step-solve.sml"

    21 ML \<open>

    22 local

    23   val thys_known_sofar = Theory.nodes_of @{theory}

    24   val isac_thys_known_sofar = take (

    25     find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,

    26     thys_known_sofar)

    27   val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar

    28 in

    29   val compare_dependencies__ThyC =

    30     if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()

    31     else raise ERROR "theory dependencies not as anticipated in ThyC"

    32 end

    33 \<close> ML \<open>

    34 \<close> ML \<open>

    35 \<close>

    36 end

author	wenzelm
	Wed, 26 May 2021 13:27:24 +0200
changeset 60282	c7b1a99bcfd2
parent 60264	b987b05f1ca8
child 60339	0d22a6bf1fc6
permissions	-rw-r--r--