Commit 697a1a45 authored by wenzelm's avatar wenzelm
Browse files

theory loader: implicit load path is considered legacy;

parent 8e6a145d3f40
(* if you'd like to build on other archive entries (here "Example"), use:
add_path "../Example";
*)
(* to suppress document generation of some theories, use:
no_document use_thys ["ThisTheory1", "ThisTheory2"];
*)
......
add_path "~~/src/HOL/Old_Number_Theory";
Thy_Load.legacy_add_path "~~/src/HOL/Old_Number_Theory";
no_document use_thys
["Factorization", "EvenOdd", "Quadratic_Reciprocity"];
......
(* $Id: ROOT.ML,v 1.3 2007-08-07 18:30:19 makarius Exp $ *)
(* License: LGPL *)
add_path "Isabelle";
add_path "Isabelle_Store";
add_path "Isa_Counter";
add_path "Isa_Counter_Store";
Thy_Load.legacy_add_path "Isabelle";
Thy_Load.legacy_add_path "Isabelle_Store";
Thy_Load.legacy_add_path "Isa_Counter";
Thy_Load.legacy_add_path "Isa_Counter_Store";
use_thys [
"TypeIds",
......
add_path "~~/src/HOL/Old_Number_Theory";
Thy_Load.legacy_add_path "~~/src/HOL/Old_Number_Theory";
no_document use_thys
["../Fermat3_4/IntNatAux", "Euler", "Quadratic_Reciprocity"];
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment