renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
authorwenzelm
Sat Jun 05 20:27:53 1999 +0200 (1999-06-05)
changeset 67839cf9c17d9e35
parent 6782 adf099e851ed
child 6784 687ddcad8581
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/auto_bind.ML
src/Pure/ROOT.ML
src/Pure/object_logic.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Jun 04 22:12:33 1999 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Jun 05 20:27:53 1999 +0200
     1.3 @@ -29,24 +29,24 @@
     1.4    General/pretty.ML General/scan.ML General/seq.ML General/source.ML \
     1.5    General/symbol.ML General/table.ML General/url.ML Interface/ROOT.ML \
     1.6    Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML \
     1.7 -  Isar/args.ML Isar/attrib.ML Isar/calculation.ML Isar/comment.ML \
     1.8 -  Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML Isar/isar_thy.ML \
     1.9 -  Isar/method.ML Isar/outer_lex.ML Isar/outer_parse.ML \
    1.10 -  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \
    1.11 -  Isar/proof_data.ML Isar/proof_history.ML Isar/session.ML \
    1.12 -  Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \
    1.13 -  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
    1.14 -  Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
    1.15 -  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
    1.16 -  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
    1.17 -  Thy/ROOT.ML Thy/browser_info.ML Thy/html.ML Thy/present.ML \
    1.18 -  Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML \
    1.19 -  Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML context.ML \
    1.20 -  deriv.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \
    1.21 -  library.ML locale.ML logic.ML net.ML object_logic.ML pattern.ML \
    1.22 -  pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML \
    1.23 -  term.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML \
    1.24 -  unify.ML
    1.25 +  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
    1.26 +  Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
    1.27 +  Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
    1.28 +  Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
    1.29 +  Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
    1.30 +  Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
    1.31 +  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \
    1.32 +  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
    1.33 +  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
    1.34 +  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
    1.35 +  Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
    1.36 +  Thy/browser_info.ML Thy/html.ML Thy/present.ML Thy/thm_database.ML \
    1.37 +  Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML \
    1.38 +  Thy/thy_syn.ML axclass.ML basis.ML context.ML deriv.ML display.ML \
    1.39 +  drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
    1.40 +  logic.ML net.ML pattern.ML pure.ML pure_thy.ML search.ML sign.ML \
    1.41 +  sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \
    1.42 +  thm.ML type.ML type_infer.ML unify.ML
    1.43  	@./mk
    1.44  
    1.45  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Fri Jun 04 22:12:33 1999 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Sat Jun 05 20:27:53 1999 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  *)
     2.5  
     2.6  (*proof engine*)
     2.7 +use "auto_bind.ML";
     2.8  use "proof_context.ML";
     2.9  use "proof.ML";
    2.10  use "proof_data.ML";
    2.11 @@ -37,6 +38,7 @@
    2.12  
    2.13  structure PureIsar =
    2.14  struct
    2.15 +  structure AutoBind = AutoBind;
    2.16    structure ProofContext = ProofContext;
    2.17    structure Proof = Proof;
    2.18    structure ProofHistory = ProofHistory;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Jun 05 20:27:53 1999 +0200
     3.3 @@ -0,0 +1,36 @@
     3.4 +(*  Title:      Pure/Isar/auto_bind.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Automatic term bindings -- logic specific patterns.
     3.9 +
    3.10 +TODO:
    3.11 +  - logic specific theory data instead of hardwired operations (!!);
    3.12 +*)
    3.13 +
    3.14 +signature AUTO_BIND =
    3.15 +sig
    3.16 +  val goal: term -> (indexname * term) list
    3.17 +  val facts: term list -> (indexname * term) list
    3.18 +end;
    3.19 +
    3.20 +structure AutoBind: AUTO_BIND =
    3.21 +struct
    3.22 +
    3.23 +val thesisN = "thesis";
    3.24 +fun thesis_name sfx = (Syntax.binding (thesisN ^ sfx), 0);
    3.25 +
    3.26 +fun goal prop =
    3.27 +  let val concl = Logic.strip_imp_concl prop in
    3.28 +    [(thesis_name "_prop", prop), (thesis_name "_concl", concl)] @
    3.29 +      (case concl of Const ("Trueprop", _) $ t => [(thesis_name "", t)] | _ => [])
    3.30 +  end;
    3.31 +
    3.32 +fun facts [] = []
    3.33 +  | facts props =
    3.34 +      (case Logic.strip_imp_concl (Library.last_elem props) of
    3.35 +        Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    3.36 +      | _ => []);
    3.37 +
    3.38 +
    3.39 +end;
     4.1 --- a/src/Pure/ROOT.ML	Fri Jun 04 22:12:33 1999 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Sat Jun 05 20:27:53 1999 +0200
     4.3 @@ -39,7 +39,6 @@
     4.4  use "theory.ML";
     4.5  use "theory_data.ML";
     4.6  use "context.ML";
     4.7 -use "object_logic.ML";
     4.8  use "thm.ML";
     4.9  use "display.ML";
    4.10  use "pure_thy.ML";
     5.1 --- a/src/Pure/object_logic.ML	Fri Jun 04 22:12:33 1999 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,37 +0,0 @@
     5.4 -(*  Title:      Pure/object_logic.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Markus Wenzel, TU Muenchen
     5.7 -
     5.8 -Object logic specific operations.
     5.9 -
    5.10 -TODO:
    5.11 -  - theory data instead of hardwired operations (!!);
    5.12 -*)
    5.13 -
    5.14 -signature OBJECT_LOGIC =
    5.15 -sig
    5.16 -  val dest_statement: string * term -> (string * term) list
    5.17 -  val dest_main_statement: term -> term
    5.18 -  val setup: (theory -> theory) list
    5.19 -end;
    5.20 -
    5.21 -structure ObjectLogic: OBJECT_LOGIC =
    5.22 -struct
    5.23 -
    5.24 -
    5.25 -fun dest_statement (name, prop) =
    5.26 -  let val concl = Logic.strip_imp_concl prop in
    5.27 -    [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
    5.28 -      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => [])
    5.29 -  end;
    5.30 -
    5.31 -fun dest_main_statement t =
    5.32 -  (case Logic.strip_imp_concl t of
    5.33 -    _ $ t => t
    5.34 -  | _ => raise TERM ("dest_main", [t]));
    5.35 -
    5.36 -
    5.37 -(* FIXME *)
    5.38 -val setup = [];
    5.39 -
    5.40 -end;