removed Main.thy
authorhaftmann
Wed Dec 27 19:09:58 2006 +0100 (2006-12-27)
changeset 21909a6439243512b
parent 21908 d02ba728cd56
child 21910 5b553ed23251
removed Main.thy
src/HOL/Integ/reflected_cooper.ML
src/HOL/ROOT.ML
src/HOL/Tools/Presburger/reflected_cooper.ML
     1.1 --- a/src/HOL/Integ/reflected_cooper.ML	Wed Dec 27 19:09:57 2006 +0100
     1.2 +++ b/src/HOL/Integ/reflected_cooper.ML	Wed Dec 27 19:09:58 2006 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4        | _ => error "qf_of_term : unknown term!";
     1.5  
     1.6  (*
     1.7 -fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT));
     1.8 +fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT));
     1.9  
    1.10  val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
    1.11  *)
     2.1 --- a/src/HOL/ROOT.ML	Wed Dec 27 19:09:57 2006 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Wed Dec 27 19:09:58 2006 +0100
     2.3 @@ -37,11 +37,6 @@
     2.4  
     2.5  with_path "Integ" use_thy "Main";
     2.6  
     2.7 -structure Main =
     2.8 -struct
     2.9 -  val thy = theory "Main"
    2.10 -end;
    2.11 -
    2.12  path_add "~~/src/HOL/Library";
    2.13  
    2.14  Goal "True";  (*leave subgoal package empty*)
     3.1 --- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Wed Dec 27 19:09:57 2006 +0100
     3.2 +++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Wed Dec 27 19:09:58 2006 +0100
     3.3 @@ -51,7 +51,7 @@
     3.4        | _ => error "qf_of_term : unknown term!";
     3.5  
     3.6  (*
     3.7 -fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT));
     3.8 +fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT));
     3.9  
    3.10  val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
    3.11  *)